or12 Show Code edit
## Rearrangement of disjuncts
thm (or12 () () (<-> (\/ ph (\/ ps ch)) (\/ ps (\/ ph ch)))
ps ch df-or
(<-> (\/ ps ch) (-> (-. ps) ch))
ph orbi2i
(<-> (\/ ph (\/ ps ch)) (\/ ph (-> (-. ps) ch)))
ph (-> (-. ps) ch) df-or
(<-> (\/ ph (-> (-. ps) ch)) (-> (-. ph) (-> (-. ps) ch)))
bitri
(<-> (\/ ph (\/ ps ch)) (-> (-. ph) (-> (-. ps) ch)))
(-. ph) (-. ps) ch bi2.04
(<-> (-> (-. ph) (-> (-. ps) ch)) (-> (-. ps) (-> (-. ph) ch)))
bitri
(<-> (\/ ph (\/ ps ch)) (-> (-. ps) (-> (-. ph) ch)))
ps (-> (-. ph) ch) df-or
(<-> (\/ ps (-> (-. ph) ch)) (-> (-. ps) (-> (-. ph) ch)))
bicomi
(<-> (-> (-. ps) (-> (-. ph) ch)) (\/ ps (-> (-. ph) ch)))
bitri
(<-> (\/ ph (\/ ps ch)) (\/ ps (-> (-. ph) ch)))
ph ch df-or
(<-> (\/ ph ch) (-> (-. ph) ch))
ps orbi2i
(<-> (\/ ps (\/ ph ch)) (\/ ps (-> (-. ph) ch)))
bicomi
(<-> (\/ ps (-> (-. ph) ch)) (\/ ps (\/ ph ch)))
bitri
(<-> (\/ ph (\/ ps ch)) (\/ ps (\/ ph ch)))
)
edit