import (PROP pax/prop () "") var (wff ps ph ch th ta) thm (a1i () ((a1i.1 ph)) (-> ps ph) (a1i.1 ph ps ax-1 ax-mp)) thm (a2i () ((a2i.1 (-> ph (-> ps ch)))) (-> (-> ph ps) (-> ph ch)) (a2i.1 ph ps ch ax-2 ax-mp)) thm (syl () ((syl.1 (-> ph ps)) (syl.2 (-> ps ch))) (-> ph ch) (syl.1 syl.2 ph a1i a2i ax-mp)) thm (com12 () ((com12.1 (-> ph (-> ps ch)))) (-> ps (-> ph ch)) (ps ph ax-1 com12.1 a2i syl)) thm (a1d () ((a1d.1 (-> ph ps))) (-> ph (-> ch ps)) (a1d.1 ch a1i com12)) thm (a2d () ((a2d.1 (-> ph (-> ps (-> ch th))))) (-> ph (-> (-> ps ch) (-> ps th))) (a2d.1 ps ch th ax-2 syl)) thm (imim2 () () (-> (-> ph ps) (-> (-> ch ph) (-> ch ps))) ((-> ph ps) ch ax-1 a2d)) thm (imim1 () () (-> (-> ph ps) (-> (-> ps ch) (-> ph ch))) (ps ch ph imim2 com12)) thm (imim2i () ((imim1i.1 (-> ph ps))) (-> (-> ch ph) (-> ch ps)) (imim1i.1 ch a1i a2i)) thm (imim1i () ((imim2i.1 (-> ph ps))) (-> (-> ps ch) (-> ph ch)) (imim2i.1 ph ps ch imim1 ax-mp)) thm (imim12i () ((imim12i.1 (-> ph ps)) (imim12i.2 (-> ch th))) (-> (-> ps ch) (-> ph th)) (imim12i.2 ps imim2i imim12i.1 th imim1i syl)) thm (3syl () ((3syl.1 (-> ph ps)) (3syl.2 (-> ps ch)) (3syl.3 (-> ch th))) (-> ph th) (3syl.1 3syl.2 syl 3syl.3 syl)) thm (syl5 () ((syl5.1 (-> ph (-> ps ch))) (syl5.2 (-> th ps))) (-> ph (-> th ch)) (syl5.1 syl5.2 ch imim1i syl)) thm (syl6 () ((syl6.1 (-> ph (-> ps ch))) (syl6.2 (-> ch th))) (-> ph (-> ps th)) (syl6.1 syl6.2 ps imim2i syl)) thm (syl7 () ((syl7.1 (-> ph (-> ps (-> ch th)))) (syl7.2 (-> ta ch))) (-> ph (-> ps (-> ta th))) (syl7.1 syl7.2 th imim1i syl6)) thm (syl8 () ((syl8.1 (-> ph (-> ps (-> ch th)))) (syl8.2 (-> th ta))) (-> ph (-> ps (-> ch ta))) (syl8.1 syl8.2 ch imim2i syl6)) thm (imim2d () ((imim1d.1 (-> ph (-> ps ch)))) (-> ph (-> (-> th ps) (-> th ch))) (imim1d.1 th a1d a2d)) thm (syld () ((syld.1 (-> ph (-> ps ch))) (syld.2 (-> ph (-> ch th)))) (-> ph (-> ps th)) (syld.1 syld.2 ps imim2d a2i ax-mp)) thm (imim1d () ((imim2d.1 (-> ph (-> ps ch)))) (-> ph (-> (-> ch th) (-> ps th))) (imim2d.1 ps ch th imim1 syl)) thm (imim12d () ((imim12d.1 (-> ph (-> ps ch))) (imim12d.2 (-> ph (-> th ta)))) (-> ph (-> (-> ch th) (-> ps ta))) (imim12d.1 th imim1d imim12d.2 ps imim2d syld)) thm (pm2.04 () () (-> (-> ph (-> ps ch)) (-> ps (-> ph ch))) (ph ps ch ax-2 ps ph ax-1 syl5)) thm (pm2.83 () () (-> (-> ph (-> ps ch)) (-> (-> ph (-> ch th)) (-> ph (-> ps th)))) (ps ch th imim1 ph imim2i a2d)) thm (com23 () ((com3.1 (-> ph (-> ps (-> ch th))))) (-> ph (-> ch (-> ps th))) (com3.1 ps ch th pm2.04 syl)) thm (com13 () ((com3.1 (-> ph (-> ps (-> ch th))))) (-> ch (-> ps (-> ph th))) (com3.1 com12 com23 com12)) thm (com3l () ((com3.1 (-> ph (-> ps (-> ch th))))) (-> ps (-> ch (-> ph th))) (com3.1 com23 com13)) thm (com3r () ((com3.1 (-> ph (-> ps (-> ch th))))) (-> ch (-> ph (-> ps th))) (com3.1 com3l com3l)) thm (com34 () ((com4.1 (-> ph (-> ps (-> ch (-> th ta)))))) (-> ph (-> ps (-> th (-> ch ta)))) (com4.1 ch th ta pm2.04 syl6)) thm (com24 () ((com4.1 (-> ph (-> ps (-> ch (-> th ta)))))) (-> ph (-> th (-> ch (-> ps ta)))) (com4.1 com34 com23 com34)) thm (com14 () ((com4.1 (-> ph (-> ps (-> ch (-> th ta)))))) (-> th (-> ps (-> ch (-> ph ta)))) (com4.1 com34 com13 com34)) thm (com4l () ((com4.1 (-> ph (-> ps (-> ch (-> th ta)))))) (-> ps (-> ch (-> th (-> ph ta)))) (com4.1 com14 com3l)) thm (com4t () ((com4.1 (-> ph (-> ps (-> ch (-> th ta)))))) (-> ch (-> th (-> ph (-> ps ta)))) (com4.1 com4l com4l)) thm (com4r () ((com4.1 (-> ph (-> ps (-> ch (-> th ta)))))) (-> th (-> ph (-> ps (-> ch ta)))) (com4.1 com4t com4l)) thm (a1dd () ((a1dd.1 (-> ph (-> ps ch)))) (-> ph (-> ps (-> th ch))) (a1dd.1 th a1d com23)) thm (mp2 () ((mp2.1 ph) (mp2.2 ps) (mp2.3 (-> ph (-> ps ch)))) ch (mp2.2 mp2.1 mp2.3 ax-mp ax-mp)) thm (mpi () ((mpi.1 ps) (mpi.2 (-> ph (-> ps ch)))) (-> ph ch) (mpi.1 mpi.2 com12 ax-mp)) thm (mpii () ((mpii.1 ch) (mpii.2 (-> ph (-> ps (-> ch th))))) (-> ph (-> ps th)) (mpii.1 mpii.2 com23 mpi)) thm (mpd () ((mpd.1 (-> ph ps)) (mpd.2 (-> ph (-> ps ch)))) (-> ph ch) (mpd.1 mpd.2 a2i ax-mp)) thm (mpdd () ((mpdd.1 (-> ph (-> ps ch))) (mpdd.2 (-> ph (-> ps (-> ch th))))) (-> ph (-> ps th)) (mpdd.1 mpdd.2 a2d mpd)) thm (mpid () ((mpid.1 (-> ph ch)) (mpid.2 (-> ph (-> ps (-> ch th))))) (-> ph (-> ps th)) (mpid.1 ps a1d mpid.2 mpdd)) thm (mpdi () ((mpdi.1 (-> ps ch)) (mpdi.2 (-> ph (-> ps (-> ch th))))) (-> ph (-> ps th)) (mpdi.1 mpdi.2 com12 mpid com12)) thm (mpcom () ((mpcom.1 (-> ps ph)) (mpcom.2 (-> ph (-> ps ch)))) (-> ps ch) (mpcom.1 mpcom.2 com12 mpd)) thm (syldd () ((syldd.1 (-> ph (-> ps (-> ch th)))) (syldd.2 (-> ph (-> ps (-> th ta))))) (-> ph (-> ps (-> ch ta))) (syldd.1 syldd.2 th ta ch imim2 syl6 mpdd)) thm (sylcom () ((sylcom.1 (-> ph (-> ps ch))) (sylcom.2 (-> ps (-> ch th)))) (-> ph (-> ps th)) (sylcom.1 com12 sylcom.2 syld com12)) thm (syl5com () ((syl5com.2 (-> ph (-> ps ch))) (syl5com.1 (-> th ps))) (-> th (-> ph ch)) (syl5com.1 ph a1d syl5com.2 sylcom)) thm (syl6com () ((syl6com.1 (-> ph (-> ps ch))) (syl6com.2 (-> ch th))) (-> ps (-> ph th)) (syl6com.1 syl6com.2 syl6 com12)) thm (syli () ((syli.1 (-> ps (-> ph ch))) (syli.2 (-> ch (-> ph th)))) (-> ps (-> ph th)) (syli.1 syli.2 com12 sylcom)) thm (syl5d () ((syl5d.1 (-> ph (-> ps (-> ch th)))) (syl5d.2 (-> ph (-> ta ch)))) (-> ph (-> ps (-> ta th))) (syl5d.1 syl5d.2 th imim1d syld)) thm (syl6d () ((syl6d.1 (-> ph (-> ps (-> ch th)))) (syl6d.2 (-> ph (-> th ta)))) (-> ph (-> ps (-> ch ta))) (syl6d.1 syl6d.2 ch imim2d syld)) thm (syl9 () ((syl9.1 (-> ph (-> ps ch))) (syl9.2 (-> th (-> ch ta)))) (-> ph (-> th (-> ps ta))) (syl9.2 ph a1i syl9.1 syl5d)) thm (syl9r () ((syl9r.1 (-> ph (-> ps ch))) (syl9r.2 (-> th (-> ch ta)))) (-> th (-> ph (-> ps ta))) (syl9r.1 syl9r.2 syl9 com12)) thm (id () () (-> ph ph) (ph ph ax-1 ph (-> ph (-> ph ph)) ax-1 mpi)) thm (id1 () () (-> ph ph) (ph ph ax-1 ph (-> ph ph) ax-1 ph (-> ph ph) ph ax-2 ax-mp ax-mp)) thm (idd () () (-> ph (-> ps ps)) (ps id ph a1i)) thm (pm2.27 () () (-> ph (-> (-> ph ps) ps)) ((-> ph ps) id com12)) thm (pm2.43 () () (-> (-> ph (-> ph ps)) (-> ph ps)) (ph ps pm2.27 a2i)) thm (pm2.43i () ((pm2.43i.1 (-> ph (-> ph ps)))) (-> ph ps) (pm2.43i.1 ph ps pm2.43 ax-mp)) thm (pm2.43d () ((pm2.43d.1 (-> ph (-> ps (-> ps ch))))) (-> ph (-> ps ch)) (pm2.43d.1 ps ch pm2.43 syl)) thm (pm2.43a () ((pm2.43a.1 (-> ps (-> ph (-> ps ch))))) (-> ps (-> ph ch)) (pm2.43a.1 com23 pm2.43i)) thm (pm2.43b () ((pm2.43a.1 (-> ps (-> ph (-> ps ch))))) (-> ph (-> ps ch)) (pm2.43a.1 pm2.43a com12)) thm (sylc () ((sylc.1 (-> ph (-> ps ch))) (sylc.2 (-> th ph)) (sylc.3 (-> th ps))) (-> th ch) (sylc.3 sylc.2 sylc.1 syl mpd)) thm (pm2.86 () () (-> (-> (-> ph ps) (-> ph ch)) (-> ph (-> ps ch))) (ps ph ax-1 (-> ph ch) imim1i com23)) thm (pm2.86i () ((pm2.86i.1 (-> (-> ph ps) (-> ph ch)))) (-> ph (-> ps ch)) (pm2.86i.1 ph ps ch pm2.86 ax-mp)) thm (pm2.86d () ((pm2.86d.1 (-> ph (-> (-> ps ch) (-> ps th))))) (-> ph (-> ps (-> ch th))) (pm2.86d.1 ps ch th pm2.86 syl)) thm (loolin () () (-> (-> (-> ph ps) (-> ps ph)) (-> ps ph)) (ps ph ax-1 (-> ps ph) imim1i pm2.43d)) thm (loowoz () () (-> (-> (-> ph ps) (-> ph ch)) (-> (-> ps ph) (-> ps ch))) (ps ph ax-1 (-> ph ch) imim1i a2d)) thm (xxxid () () (-> ph ph) (ph id)) thm (a3i () ((a3i.1 (-> (-. ph) (-. ps)))) (-> ps ph) (a3i.1 ph ps ax-3 ax-mp)) thm (a3d () ((a3d.1 (-> ph (-> (-. ps) (-. ch))))) (-> ph (-> ch ps)) (a3d.1 ps ch ax-3 syl)) thm (pm2.21 () () (-> (-. ph) (-> ph ps)) ((-. ph) (-. ps) ax-1 a3d)) thm (pm2.24 () () (-> ph (-> (-. ph) ps)) (ph ps pm2.21 com12)) thm (pm2.21i () ((pm2.21i.1 (-. ph))) (-> ph ps) (pm2.21i.1 (-. ps) a1i a3i)) thm (pm2.21d () ((pm2.21d.1 (-> ph (-. ps)))) (-> ph (-> ps ch)) (pm2.21d.1 (-. ch) a1d a3d)) thm (pm2.18 () () (-> (-> (-. ph) ph) ph) (ph (-. (-> (-. ph) ph)) pm2.21 a2i a3d pm2.43i)) thm (peirce () () (-> (-> (-> ph ps) ph) ph) (ph ps pm2.21 ph imim1i ph pm2.18 syl)) thm (looinv () () (-> (-> (-> ph ps) ps) (-> (-> ps ph) ph)) ((-> ph ps) ps ph imim1 ph ps peirce syl6)) thm (nega () () (-> (-. (-. ph)) ph) ((-. ph) ph pm2.21 ph pm2.18 syl)) thm (negb () () (-> ph (-. (-. ph))) ((-. ph) nega a3i)) thm (pm2.01 () () (-> (-> ph (-. ph)) (-. ph)) (ph nega (-. ph) imim1i (-. ph) pm2.18 syl)) thm (pm2.01d () ((pm2.01d.1 (-> ph (-> ps (-. ps))))) (-> ph (-. ps)) (pm2.01d.1 ps pm2.01 syl)) thm (con2 () () (-> (-> ph (-. ps)) (-> ps (-. ph))) (ph nega (-. ps) imim1i a3d)) thm (con2d () ((con2d.1 (-> ph (-> ps (-. ch))))) (-> ph (-> ch (-. ps))) (con2d.1 ps ch con2 syl)) thm (con1 () () (-> (-> (-. ph) ps) (-> (-. ps) ph)) (ps negb (-. ph) imim2i a3d)) thm (con1d () ((con1d.1 (-> ph (-> (-. ps) ch)))) (-> ph (-> (-. ch) ps)) (con1d.1 ps ch con1 syl)) thm (con3 () () (-> (-> ph ps) (-> (-. ps) (-. ph))) (ps negb ph imim2i con2d)) thm (con3d () ((con3d.1 (-> ph (-> ps ch)))) (-> ph (-> (-. ch) (-. ps))) (con3d.1 ps ch con3 syl)) thm (con1i () ((con1.a (-> (-. ph) ps))) (-> (-. ps) ph) (con1.a ps negb syl a3i)) thm (con2i () ((con2.a (-> ph (-. ps)))) (-> ps (-. ph)) (ph nega con2.a syl a3i)) thm (con3i () ((con3.a (-> ph ps))) (-> (-. ps) (-. ph)) (ph nega con3.a syl con1i)) thm (pm2.36 () () (-> (-> ps ch) (-> (-> (-. ph) ps) (-> (-. ch) ph))) (ps ch (-. ph) imim2 ph ch con1 syl6)) thm (pm2.37 () () (-> (-> ps ch) (-> (-> (-. ps) ph) (-> (-. ph) ch))) (ps ph con1 ch imim1d com12)) thm (pm2.38 () () (-> (-> ps ch) (-> (-> (-. ps) ph) (-> (-. ch) ph))) (ps ch con3 ph imim1d)) thm (pm2.5 () () (-> (-. (-> ph ps)) (-> (-. ph) ps)) (ph ps pm2.21 con3i ps pm2.21d)) thm (pm2.51 () () (-> (-. (-> ph ps)) (-> ph (-. ps))) (ps ph ax-1 con3i ph a1d)) thm (pm2.52 () () (-> (-. (-> ph ps)) (-> (-. ph) (-. ps))) (ps ph ax-1 con3i (-. ph) a1d)) thm (pm2.521 () () (-> (-. (-> ph ps)) (-> ps ph)) (ph ps pm2.52 a3d)) thm (pm2.21ni () ((pm2.21ni.1 ph)) (-> (-. ph) ps) (pm2.21ni.1 (-. ps) a1i con1i)) thm (mto () ((mto.1 (-. ps)) (mto.2 (-> ph ps))) (-. ph) (mto.1 mto.2 con3i ax-mp)) thm (mtoi () ((mtoi.1 (-. ch)) (mtoi.2 (-> ph (-> ps ch)))) (-> ph (-. ps)) (mtoi.1 mtoi.2 con3d mpi)) thm (mtod () ((mtod.1 (-> ph (-. ch))) (mtod.2 (-> ph (-> ps ch)))) (-> ph (-. ps)) (mtod.1 mtod.2 con3d mpd)) thm (mt2 () ((mt2.1 ps) (mt2.2 (-> ph (-. ps)))) (-. ph) (mt2.1 mt2.2 con2i ax-mp)) thm (mt2i () ((mt2i.1 ch) (mt2i.2 (-> ph (-> ps (-. ch))))) (-> ph (-. ps)) (mt2i.1 mt2i.2 con2d mpi)) thm (mt2d () ((mt2d.1 (-> ph ch)) (mt2d.2 (-> ph (-> ps (-. ch))))) (-> ph (-. ps)) (mt2d.1 mt2d.2 con2d mpd)) thm (mt3 () ((mt3.1 (-. ps)) (mt3.2 (-> (-. ph) ps))) ph (mt3.1 mt3.2 con1i ax-mp)) thm (mt3i () ((mt3i.1 (-. ch)) (mt3i.2 (-> ph (-> (-. ps) ch)))) (-> ph ps) (mt3i.1 mt3i.2 con1d mpi)) thm (mt3d () ((mt3d.1 (-> ph (-. ch))) (mt3d.2 (-> ph (-> (-. ps) ch)))) (-> ph ps) (mt3d.1 mt3d.2 con1d mpd)) thm (nsyl () ((nsyl.1 (-> ph (-. ps))) (nsyl.2 (-> ch ps))) (-> ph (-. ch)) (nsyl.1 nsyl.2 con3i syl)) thm (nsyld () ((nsyld.1 (-> ph (-> ps (-. ch)))) (nsyld.2 (-> ph (-> ta ch)))) (-> ph (-> ps (-. ta))) (nsyld.1 nsyld.2 con3d syld)) thm (nsyl2 () ((nsyl2.1 (-> ph (-. ps))) (nsyl2.2 (-> (-. ch) ps))) (-> ph ch) (nsyl2.1 nsyl2.2 con1i syl)) thm (nsyl3 () ((nsyl3.1 (-> ph (-. ps))) (nsyl3.2 (-> ch ps))) (-> ch (-. ph)) (nsyl3.2 nsyl3.1 con2i syl)) thm (nsyl4 () ((nsyl4.1 (-> ph ps)) (nsyl4.2 (-> (-. ph) ch))) (-> (-. ch) ps) (nsyl4.2 con1i nsyl4.1 syl)) thm (nsyli () ((nsyli.1 (-> ph (-> ps ch))) (nsyli.2 (-> th (-. ch)))) (-> ph (-> th (-. ps))) (nsyli.1 con3d nsyli.2 syl5)) thm (pm3.2im () () (-> ph (-> ps (-. (-> ph (-. ps))))) (ph (-. ps) pm2.27 con2d)) thm (mth8 () () (-> ph (-> (-. ps) (-. (-> ph ps)))) (ph ps pm2.27 con3d)) thm (pm2.61 () () (-> (-> ph ps) (-> (-> (-. ph) ps) ps)) (ph ps (-. ps) imim2 ps pm2.18 syl6 ph ps con1 syl5)) thm (pm2.61i () ((pm2.61i.1 (-> ph ps)) (pm2.61i.2 (-> (-. ph) ps))) ps (pm2.61i.1 pm2.61i.2 ph ps pm2.61 mp2)) thm (pm2.61d () ((pm2.61d.1 (-> ph (-> ps ch))) (pm2.61d.2 (-> ph (-> (-. ps) ch)))) (-> ph ch) (pm2.61d.1 com12 pm2.61d.2 com12 pm2.61i)) thm (pm2.61d1 () ((pm2.61d1.1 (-> ph (-> ps ch))) (pm2.61d1.2 (-> (-. ps) ch))) (-> ph ch) (pm2.61d1.1 pm2.61d1.2 ph a1i pm2.61d)) thm (pm2.61d2 () ((pm2.61d2.1 (-> ph (-> (-. ps) ch))) (pm2.61d2.2 (-> ps ch))) (-> ph ch) (pm2.61d2.2 ph a1i pm2.61d2.1 pm2.61d)) thm (pm2.61ii () ((pm2.61ii.1 (-> (-. ph) (-> (-. ps) ch))) (pm2.61ii.2 (-> ph ch)) (pm2.61ii.3 (-> ps ch))) ch (pm2.61ii.2 pm2.61ii.1 pm2.61ii.3 pm2.61d2 pm2.61i)) thm (pm2.61nii () ((pm2.61nii.1 (-> ph (-> ps ch))) (pm2.61nii.2 (-> (-. ph) ch)) (pm2.61nii.3 (-> (-. ps) ch))) ch (pm2.61nii.1 com12 pm2.61nii.2 pm2.61d1 pm2.61nii.3 pm2.61i)) thm (pm2.61iii () ((pm2.61iii.1 (-> (-. ph) (-> (-. ps) (-> (-. ch) th)))) (pm2.61iii.2 (-> ph th)) (pm2.61iii.3 (-> ps th)) (pm2.61iii.4 (-> ch th))) th (pm2.61iii.2 (-. ch) a1d (-. ps) a1d pm2.61iii.1 pm2.61i pm2.61iii.3 pm2.61iii.4 pm2.61ii)) thm (pm2.6 () () (-> (-> (-. ph) ps) (-> (-> ph ps) ps)) (ph ps pm2.61 com12)) thm (pm2.65 () () (-> (-> ph ps) (-> (-> ph (-. ps)) (-. ph))) (ph ps pm3.2im a2i con2d)) thm (pm2.65i () ((pm2.65i.1 (-> ph ps)) (pm2.65i.2 (-> ph (-. ps)))) (-. ph) (pm2.65i.2 pm2.65i.1 nsyl ph pm2.01 ax-mp)) thm (pm2.65d () ((pm2.65d.1 (-> ph (-> ps ch))) (pm2.65d.2 (-> ph (-> ps (-. ch))))) (-> ph (-. ps)) (ps ch pm2.65 pm2.65d.1 pm2.65d.2 sylc)) thm (ja () ((ja.1 (-> (-. ph) ch)) (ja.2 (-> ps ch))) (-> (-> ph ps) ch) (ph ps pm2.27 ja.2 syl6 ja.1 (-> ph ps) a1d pm2.61i)) thm (jc () ((jc.1 (-> ph ps)) (jc.2 (-> ph ch))) (-> ph (-. (-> ps (-. ch)))) (ps ch pm3.2im jc.1 jc.2 sylc)) thm (pm3.26im () () (-> (-. (-> ph (-. ps))) ph) (ph (-. ps) pm2.21 con1i)) thm (pm3.27im () () (-> (-. (-> ph (-. ps))) ps) ((-. ps) ph ax-1 con1i)) thm (impt () () (-> (-> ph (-> ps ch)) (-> (-. (-> ph (-. ps))) ch)) (ps ch con3 ph imim2i com23 con1d)) thm (expt () () (-> (-> (-. (-> ph (-. ps))) ch) (-> ph (-> ps ch))) (ph ps pm3.2im ch imim1d com12)) thm (impi () ((impi.1 (-> ph (-> ps ch)))) (-> (-. (-> ph (-. ps))) ch) (impi.1 ph ps ch impt ax-mp)) thm (expi () ((expi.1 (-> (-. (-> ph (-. ps))) ch))) (-> ph (-> ps ch)) (expi.1 ph ps ch expt ax-mp)) thm (bijust () () (-. (-> (-> ph ph) (-. (-> ph ph)))) (ph id (-> ph ph) pm2.01 mt2)) thm (biigb () () (<-> (<-> ph ps) (-. (-> (-> ph ps) (-. (-> ps ph))))) (ph ps df-bi ch th ax-1 (-. (-> (-. (-> (-> (<-> ph ps) (-. (-> (-> ph ps) (-. (-> ps ph))))) (-. (-> (-. (-> (-> ph ps) (-. (-> ps ph)))) (<-> ph ps))))) (<-> (<-> ph ps) (-. (-> (-> ph ps) (-. (-> ps ph))))))) (-> (<-> (<-> ph ps) (-. (-> (-> ph ps) (-. (-> ps ph))))) (-. (-> (-> (<-> ph ps) (-. (-> (-> ph ps) (-. (-> ps ph))))) (-. (-> (-. (-> (-> ph ps) (-. (-> ps ph)))) (<-> ph ps)))))) ax-1 (<-> ph ps) (-. (-> (-> ph ps) (-. (-> ps ph)))) df-bi (-. (-> (-> (<-> (<-> ph ps) (-. (-> (-> ph ps) (-. (-> ps ph))))) (-. (-> (-> (<-> ph ps) (-. (-> (-> ph ps) (-. (-> ps ph))))) (-. (-> (-. (-> (-> ph ps) (-. (-> ps ph)))) (<-> ph ps)))))) (-. (-> (-. (-> (-> (<-> ph ps) (-. (-> (-> ph ps) (-. (-> ps ph))))) (-. (-> (-. (-> (-> ph ps) (-. (-> ps ph)))) (<-> ph ps))))) (<-> (<-> ph ps) (-. (-> (-> ph ps) (-. (-> ps ph))))))))) (-. (-. (-> ch (-> th ch)))) ax-1 ax-mp (-. (-> ch (-> th ch))) (-> (-> (<-> (<-> ph ps) (-. (-> (-> ph ps) (-. (-> ps ph))))) (-. (-> (-> (<-> ph ps) (-. (-> (-> ph ps) (-. (-> ps ph))))) (-. (-> (-. (-> (-> ph ps) (-. (-> ps ph)))) (<-> ph ps)))))) (-. (-> (-. (-> (-> (<-> ph ps) (-. (-> (-> ph ps) (-. (-> ps ph))))) (-. (-> (-. (-> (-> ph ps) (-. (-> ps ph)))) (<-> ph ps))))) (<-> (<-> ph ps) (-. (-> (-> ph ps) (-. (-> ps ph)))))))) ax-3 ax-mp (-> (-> (-> (<-> (<-> ph ps) (-. (-> (-> ph ps) (-. (-> ps ph))))) (-. (-> (-> (<-> ph ps) (-. (-> (-> ph ps) (-. (-> ps ph))))) (-. (-> (-. (-> (-> ph ps) (-. (-> ps ph)))) (<-> ph ps)))))) (-. (-> (-. (-> (-> (<-> ph ps) (-. (-> (-> ph ps) (-. (-> ps ph))))) (-. (-> (-. (-> (-> ph ps) (-. (-> ps ph)))) (<-> ph ps))))) (<-> (<-> ph ps) (-. (-> (-> ph ps) (-. (-> ps ph)))))))) (-. (-> ch (-> th ch)))) (-. (-> (-. (-> (-> (<-> ph ps) (-. (-> (-> ph ps) (-. (-> ps ph))))) (-. (-> (-. (-> (-> ph ps) (-. (-> ps ph)))) (<-> ph ps))))) (<-> (<-> ph ps) (-. (-> (-> ph ps) (-. (-> ps ph))))))) ax-1 ax-mp (-. (-> (-. (-> (-> (<-> ph ps) (-. (-> (-> ph ps) (-. (-> ps ph))))) (-. (-> (-. (-> (-> ph ps) (-. (-> ps ph)))) (<-> ph ps))))) (<-> (<-> ph ps) (-. (-> (-> ph ps) (-. (-> ps ph))))))) (-> (-> (<-> (<-> ph ps) (-. (-> (-> ph ps) (-. (-> ps ph))))) (-. (-> (-> (<-> ph ps) (-. (-> (-> ph ps) (-. (-> ps ph))))) (-. (-> (-. (-> (-> ph ps) (-. (-> ps ph)))) (<-> ph ps)))))) (-. (-> (-. (-> (-> (<-> ph ps) (-. (-> (-> ph ps) (-. (-> ps ph))))) (-. (-> (-. (-> (-> ph ps) (-. (-> ps ph)))) (<-> ph ps))))) (<-> (<-> ph ps) (-. (-> (-> ph ps) (-. (-> ps ph)))))))) (-. (-> ch (-> th ch))) ax-2 ax-mp ax-mp (-> (-. (-> (-> (<-> ph ps) (-. (-> (-> ph ps) (-. (-> ps ph))))) (-. (-> (-. (-> (-> ph ps) (-. (-> ps ph)))) (<-> ph ps))))) (<-> (<-> ph ps) (-. (-> (-> ph ps) (-. (-> ps ph)))))) (-> ch (-> th ch)) ax-3 ax-mp ax-mp ax-mp)) thm (bi1 () () (-> (<-> ph ps) (-> ph ps)) (ph ps df-bi (-> (<-> ph ps) (-. (-> (-> ph ps) (-. (-> ps ph))))) (-> (-. (-> (-> ph ps) (-. (-> ps ph)))) (<-> ph ps)) pm3.26im ax-mp (-> ph ps) (-> ps ph) pm3.26im syl)) thm (bi2 () () (-> (<-> ph ps) (-> ps ph)) (ph ps df-bi (-> (<-> ph ps) (-. (-> (-> ph ps) (-. (-> ps ph))))) (-> (-. (-> (-> ph ps) (-. (-> ps ph)))) (<-> ph ps)) pm3.26im ax-mp (-> ph ps) (-> ps ph) pm3.27im syl)) thm (bi3 () () (-> (-> ph ps) (-> (-> ps ph) (<-> ph ps))) (ph ps df-bi (-> (<-> ph ps) (-. (-> (-> ph ps) (-. (-> ps ph))))) (-> (-. (-> (-> ph ps) (-. (-> ps ph)))) (<-> ph ps)) pm3.27im ax-mp expi)) thm (biimp () ((biimp.1 (<-> ph ps))) (-> ph ps) (biimp.1 ph ps bi1 ax-mp)) thm (biimpr () ((biimpr.1 (<-> ph ps))) (-> ps ph) (biimpr.1 ph ps bi2 ax-mp)) thm (biimpd () ((biimpd.1 (-> ph (<-> ps ch)))) (-> ph (-> ps ch)) (biimpd.1 ps ch bi1 syl)) thm (biimprd () ((biimpd.1 (-> ph (<-> ps ch)))) (-> ph (-> ch ps)) (biimpd.1 ps ch bi2 syl)) thm (biimpcd () ((biimpd.1 (-> ph (<-> ps ch)))) (-> ps (-> ph ch)) (biimpd.1 biimpd com12)) thm (biimprcd () ((biimpd.1 (-> ph (<-> ps ch)))) (-> ch (-> ph ps)) (biimpd.1 biimprd com12)) thm (impbi () ((impbi.1 (-> ph ps)) (impbi.2 (-> ps ph))) (<-> ph ps) (impbi.1 impbi.2 ph ps bi3 mp2)) thm (bii () () (<-> (<-> ph ps) (-. (-> (-> ph ps) (-. (-> ps ph))))) (ph ps bi1 ph ps bi2 jc ph ps bi3 impi impbi)) thm (bi2.04 () () (<-> (-> ph (-> ps ch)) (-> ps (-> ph ch))) (ph ps ch pm2.04 ps ph ch pm2.04 impbi)) thm (pm4.13 () () (<-> ph (-. (-. ph))) (ph negb ph nega impbi)) thm (pm4.8 () () (<-> (-> ph (-. ph)) (-. ph)) (ph pm2.01 (-. ph) ph ax-1 impbi)) thm (pm4.81 () () (<-> (-> (-. ph) ph) ph) (ph pm2.18 ph ph pm2.24 impbi)) thm (pm4.1 () () (<-> (-> ph ps) (-> (-. ps) (-. ph))) (ph ps con3 ps ph ax-3 impbi)) thm (bi2.03 () () (<-> (-> ph (-. ps)) (-> ps (-. ph))) (ph ps con2 ps ph con2 impbi)) thm (bi2.15 () () (<-> (-> (-. ph) ps) (-> (-. ps) ph)) (ph ps con1 ps ph con1 impbi)) thm (pm5.4 () () (<-> (-> ph (-> ph ps)) (-> ph ps)) (ph ps pm2.43 (-> ph ps) ph ax-1 impbi)) thm (imdi () () (<-> (-> ph (-> ps ch)) (-> (-> ph ps) (-> ph ch))) (ph ps ch ax-2 ph ps ch pm2.86 impbi)) thm (pm5.41 () () (<-> (-> (-> ph ps) (-> ph ch)) (-> ph (-> ps ch))) (ph ps ch pm2.86 ph ps ch ax-2 impbi)) thm (pm4.2 () () (<-> ph ph) (ph id ph id impbi)) thm (pm4.2i () () (-> ph (<-> ps ps)) (ps pm4.2 ph a1i)) thm (bicomi () ((bicom.1 (<-> ph ps))) (<-> ps ph) (bicom.1 biimpr bicom.1 biimp impbi)) thm (bitr () ((bitr.1 (<-> ph ps)) (bitr.2 (<-> ps ch))) (<-> ph ch) (bitr.1 biimp bitr.2 biimp syl bitr.2 biimpr bitr.1 biimpr syl impbi)) thm (bitr2 () ((bitr2.1 (<-> ph ps)) (bitr2.2 (<-> ps ch))) (<-> ch ph) (bitr2.1 bitr2.2 bitr bicomi)) thm (bitr3 () ((bitr3.1 (<-> ps ph)) (bitr3.2 (<-> ps ch))) (<-> ph ch) (bitr3.1 bicomi bitr3.2 bitr)) thm (bitr4 () ((bitr4.1 (<-> ph ps)) (bitr4.2 (<-> ch ps))) (<-> ph ch) (bitr4.1 bitr4.2 bicomi bitr)) thm (3bitr () ((3bitr.1 (<-> ph ps)) (3bitr.2 (<-> ps ch)) (3bitr.3 (<-> ch th))) (<-> ph th) (3bitr.1 3bitr.2 3bitr.3 bitr bitr)) thm (3bitr3 () ((3bitr3.1 (<-> ph ps)) (3bitr3.2 (<-> ph ch)) (3bitr3.3 (<-> ps th))) (<-> ch th) (3bitr3.2 3bitr3.1 bitr3 3bitr3.3 bitr)) thm (3bitr3r () ((3bitr3.1 (<-> ph ps)) (3bitr3.2 (<-> ph ch)) (3bitr3.3 (<-> ps th))) (<-> th ch) (3bitr3.3 3bitr3.1 3bitr3.2 bitr3 bitr3)) thm (3bitr4 () ((3bitr4.1 (<-> ph ps)) (3bitr4.2 (<-> ch ph)) (3bitr4.3 (<-> th ps))) (<-> ch th) (3bitr4.2 3bitr4.1 3bitr4.3 bitr4 bitr)) thm (3bitr4r () ((3bitr4.1 (<-> ph ps)) (3bitr4.2 (<-> ch ph)) (3bitr4.3 (<-> th ps))) (<-> th ch) (3bitr4.2 3bitr4.1 3bitr4.3 bitr4 bitr2)) thm (imbi2i () ((bi.a (<-> ph ps))) (<-> (-> ch ph) (-> ch ps)) (bi.a biimp ch imim2i bi.a biimpr ch imim2i impbi)) thm (imbi1i () ((bi.a (<-> ph ps))) (<-> (-> ph ch) (-> ps ch)) (bi.a biimpr ch imim1i bi.a biimp ch imim1i impbi)) thm (negbii () ((bi.a (<-> ph ps))) (<-> (-. ph) (-. ps)) (bi.a biimpr con3i bi.a biimp con3i impbi)) thm (imbi12i () ((bi2im.1 (<-> ph ps)) (bi2im.2 (<-> ch th))) (<-> (-> ph ch) (-> ps th)) (bi2im.2 ph imbi2i bi2im.1 th imbi1i bitr)) thm (mpbi () ((mpbi.min ph) (mpbi.maj (<-> ph ps))) ps (mpbi.min mpbi.maj biimp ax-mp)) thm (mpbir () ((mpbir.min ps) (mpbir.maj (<-> ph ps))) ph (mpbir.min mpbir.maj biimpr ax-mp)) thm (mtbi () ((mtbi.1 (-. ph)) (mtbi.2 (<-> ph ps))) (-. ps) (mtbi.1 mtbi.2 negbii mpbi)) thm (mtbir () ((mtbir.1 (-. ps)) (mtbir.2 (<-> ph ps))) (-. ph) (mtbir.1 mtbir.2 negbii mpbir)) thm (mpbii () ((mpbii.min ps) (mpbii.maj (-> ph (<-> ps ch)))) (-> ph ch) (mpbii.min mpbii.maj biimpd mpi)) thm (mpbiri () ((mpbiri.min ch) (mpbiri.maj (-> ph (<-> ps ch)))) (-> ph ps) (mpbiri.min mpbiri.maj biimprd mpi)) thm (mpbid () ((mpbid.min (-> ph ps)) (mpbid.maj (-> ph (<-> ps ch)))) (-> ph ch) (mpbid.min mpbid.maj biimpd mpd)) thm (mpbird () ((mpbird.min (-> ph ch)) (mpbird.maj (-> ph (<-> ps ch)))) (-> ph ps) (mpbird.min mpbird.maj biimprd mpd)) thm (a1bi () ((a1bi.1 ph)) (<-> ps (-> ph ps)) (ps ph ax-1 a1bi.1 ph ps pm2.27 ax-mp impbi)) thm (sylib () ((sylib.1 (-> ph ps)) (sylib.2 (<-> ps ch))) (-> ph ch) (sylib.1 sylib.2 biimp syl)) thm (sylbi () ((sylbi.1 (<-> ph ps)) (sylbi.2 (-> ps ch))) (-> ph ch) (sylbi.1 biimp sylbi.2 syl)) thm (sylibr () ((sylibr.1 (-> ph ps)) (sylibr.2 (<-> ch ps))) (-> ph ch) (sylibr.1 sylibr.2 biimpr syl)) thm (sylbir () ((sylbir.1 (<-> ps ph)) (sylbir.2 (-> ps ch))) (-> ph ch) (sylbir.1 biimpr sylbir.2 syl)) thm (sylibd () ((sylibd.1 (-> ph (-> ps ch))) (sylibd.2 (-> ph (<-> ch th)))) (-> ph (-> ps th)) (sylibd.1 sylibd.2 biimpd syld)) thm (sylbid () ((sylbid.1 (-> ph (<-> ps ch))) (sylbid.2 (-> ph (-> ch th)))) (-> ph (-> ps th)) (sylbid.1 biimpd sylbid.2 syld)) thm (sylibrd () ((sylibrd.1 (-> ph (-> ps ch))) (sylibrd.2 (-> ph (<-> th ch)))) (-> ph (-> ps th)) (sylibrd.1 sylibrd.2 biimprd syld)) thm (sylbird () ((sylbird.1 (-> ph (<-> ch ps))) (sylbird.2 (-> ph (-> ch th)))) (-> ph (-> ps th)) (sylbird.1 biimprd sylbird.2 syld)) thm (syl5ib () ((syl5ib.1 (-> ph (-> ps ch))) (syl5ib.2 (<-> th ps))) (-> ph (-> th ch)) (syl5ib.1 syl5ib.2 biimp syl5)) thm (syl5ibr () ((syl5ibr.1 (-> ph (-> ps ch))) (syl5ibr.2 (<-> ps th))) (-> ph (-> th ch)) (syl5ibr.1 syl5ibr.2 biimpr syl5)) thm (syl5bi () ((syl5bi.1 (-> ph (<-> ps ch))) (syl5bi.2 (-> th ps))) (-> ph (-> th ch)) (syl5bi.1 biimpd syl5bi.2 syl5)) thm (syl5bir () ((syl5bir.1 (-> ph (<-> ps ch))) (syl5bir.2 (-> th ch))) (-> ph (-> th ps)) (syl5bir.1 biimprd syl5bir.2 syl5)) thm (syl6ib () ((syl6ib.1 (-> ph (-> ps ch))) (syl6ib.2 (<-> ch th))) (-> ph (-> ps th)) (syl6ib.1 syl6ib.2 biimp syl6)) thm (syl6ibr () ((syl6ibr.1 (-> ph (-> ps ch))) (syl6ibr.2 (<-> th ch))) (-> ph (-> ps th)) (syl6ibr.1 syl6ibr.2 biimpr syl6)) thm (syl6bi () ((syl6bi.1 (-> ph (<-> ps ch))) (syl6bi.2 (-> ch th))) (-> ph (-> ps th)) (syl6bi.1 biimpd syl6bi.2 syl6)) thm (syl6bir () ((syl6bir.1 (-> ph (<-> ch ps))) (syl6bir.2 (-> ch th))) (-> ph (-> ps th)) (syl6bir.1 biimprd syl6bir.2 syl6)) thm (bisyl7 () ((bisyl7.1 (-> ph (-> ps (-> ch th)))) (bisyl7.2 (<-> ta ch))) (-> ph (-> ps (-> ta th))) (bisyl7.1 bisyl7.2 biimp syl7)) thm (bisyl8 () ((bisyl8.1 (-> ph (-> ps (-> ch th)))) (bisyl8.2 (<-> th ta))) (-> ph (-> ps (-> ch ta))) (bisyl8.1 bisyl8.2 biimp syl8)) thm (3imtr3 () ((3imtr3.1 (-> ph ps)) (3imtr3.2 (<-> ph ch)) (3imtr3.3 (<-> ps th))) (-> ch th) (3imtr3.2 3imtr3.1 sylbir 3imtr3.3 sylib)) thm (3imtr4 () ((3imtr4.1 (-> ph ps)) (3imtr4.2 (<-> ch ph)) (3imtr4.3 (<-> th ps))) (-> ch th) (3imtr4.2 3imtr4.1 sylbi 3imtr4.3 sylibr)) thm (bicon1i () ((bicon1.1 (<-> (-. ph) ps))) (<-> (-. ps) ph) (bicon1.1 biimp con1i bicon1.1 biimpr con2i impbi)) thm (bicon2i () ((bicon2.1 (<-> ph (-. ps)))) (<-> ps (-. ph)) (bicon2.1 bicomi bicon1i bicomi)) thm (pm4.64 () () (<-> (-> (-. ph) ps) (\/ ph ps)) (ph ps df-or bicomi)) thm (pm2.54 () () (-> (-> (-. ph) ps) (\/ ph ps)) (ph ps df-or biimpr)) thm (pm4.63 () () (<-> (-. (-> ph (-. ps))) (/\ ph ps)) (ph ps df-an bicomi)) thm (dfor2 () () (<-> (\/ ph ps) (-> (-> ph ps) ps)) (ph ps df-or ph ps pm2.6 ph ps pm2.21 ps imim1i impbi bitr)) thm (ori () ((ori.1 (\/ ph ps))) (-> (-. ph) ps) (ori.1 ph ps df-or mpbi)) thm (orri () ((orri.1 (-> (-. ph) ps))) (\/ ph ps) (orri.1 ph ps df-or mpbir)) thm (ord () ((ord.1 (-> ph (\/ ps ch)))) (-> ph (-> (-. ps) ch)) (ord.1 ps ch df-or sylib)) thm (orrd () ((orrd.1 (-> ph (-> (-. ps) ch)))) (-> ph (\/ ps ch)) (orrd.1 ps ch df-or sylibr)) thm (imor () () (<-> (-> ph ps) (\/ (-. ph) ps)) (ph pm4.13 ps imbi1i (-. ph) ps df-or bitr4)) thm (pm4.62 () () (<-> (-> ph (-. ps)) (\/ (-. ph) (-. ps))) (ph (-. ps) imor)) thm (pm4.66 () () (<-> (-> (-. ph) (-. ps)) (\/ ph (-. ps))) (ph (-. ps) pm4.64)) thm (iman () () (<-> (-> ph ps) (-. (/\ ph (-. ps)))) (ps pm4.13 ph imbi2i ph (-. ps) df-an bicon2i bitr)) thm (annim () () (<-> (/\ ph (-. ps)) (-. (-> ph ps))) (ph ps iman bicon2i)) thm (pm4.61 () () (<-> (-. (-> ph ps)) (/\ ph (-. ps))) (ph ps annim bicomi)) thm (pm4.65 () () (<-> (-. (-> (-. ph) ps)) (/\ (-. ph) (-. ps))) ((-. ph) ps pm4.61)) thm (pm4.67 () () (<-> (-. (-> (-. ph) (-. ps))) (/\ (-. ph) ps)) ((-. ph) ps pm4.63)) thm (imnan () () (<-> (-> ph (-. ps)) (-. (/\ ph ps))) (ph ps df-an bicon2i)) thm (oridm () () (<-> (\/ ph ph) ph) (ph ph df-or ph ph pm2.24 ph pm2.18 impbi bitr4)) thm (pm4.25 () () (<-> ph (\/ ph ph)) (ph oridm bicomi)) thm (pm1.2 () () (-> (\/ ph ph) ph) (ph oridm biimp)) thm (orcom () () (<-> (\/ ph ps) (\/ ps ph)) (ph ps bi2.15 ph ps df-or ps ph df-or 3bitr4)) thm (pm1.4 () () (-> (\/ ph ps) (\/ ps ph)) (ph ps orcom biimp)) thm (pm2.62 () () (-> (\/ ph ps) (-> (-> ph ps) ps)) (ph ps dfor2 biimp)) thm (pm2.621 () () (-> (-> ph ps) (-> (\/ ph ps) ps)) (ph ps pm2.62 com12)) thm (pm2.68 () () (-> (-> (-> ph ps) ps) (\/ ph ps)) (ph ps dfor2 biimpr)) thm (orel1 () () (-> (-. ph) (-> (\/ ph ps) ps)) (ph ps df-or biimp com12)) thm (orel2 () () (-> (-. ph) (-> (\/ ps ph) ps)) (ph ps orel1 ps ph orcom syl5ib)) thm (pm2.25 () () (\/ ph (-> (\/ ph ps) ps)) (ph ps orel1 orri)) thm (pm2.53 () () (-> (\/ ph ps) (-> (-. ph) ps)) (ph ps orel1 com12)) thm (orbi2i () ((bi.oa (<-> ph ps))) (<-> (\/ ch ph) (\/ ch ps)) (bi.oa (-. ch) imbi2i ch ph df-or ch ps df-or 3bitr4)) thm (orbi1i () ((bi.oa (<-> ph ps))) (<-> (\/ ph ch) (\/ ps ch)) (ph ch orcom bi.oa ch orbi2i ch ps orcom 3bitr)) thm (orbi12i () ((bi2or.1 (<-> ph ps)) (bi2or.2 (<-> ch th))) (<-> (\/ ph ch) (\/ ps th)) (bi2or.2 ph orbi2i bi2or.1 th orbi1i bitr)) thm (or12 () () (<-> (\/ ph (\/ ps ch)) (\/ ps (\/ ph ch))) ((-. ps) (-. ph) ch bi2.04 ph ch df-or (-. ps) imbi2i ps ch df-or (-. ph) imbi2i 3bitr4r ph (\/ ps ch) df-or ps (\/ ph ch) df-or 3bitr4)) thm (pm1.5 () () (-> (\/ ph (\/ ps ch)) (\/ ps (\/ ph ch))) (ph ps ch or12 biimp)) thm (orass () () (<-> (\/ (\/ ph ps) ch) (\/ ph (\/ ps ch))) (ch ph ps or12 (\/ ph ps) ch orcom ps ch orcom ph orbi2i 3bitr4)) thm (pm2.31 () () (-> (\/ ph (\/ ps ch)) (\/ (\/ ph ps) ch)) (ph ps ch orass biimpr)) thm (pm2.32 () () (-> (\/ (\/ ph ps) ch) (\/ ph (\/ ps ch))) (ph ps ch orass biimp)) thm (or23 () () (<-> (\/ (\/ ph ps) ch) (\/ (\/ ph ch) ps)) (ps ch orcom ph orbi2i ph ps ch orass ph ch ps orass 3bitr4)) thm (or4 () () (<-> (\/ (\/ ph ps) (\/ ch th)) (\/ (\/ ph ch) (\/ ps th))) (ps ch th or12 ph orbi2i ph ps (\/ ch th) orass ph ch (\/ ps th) orass 3bitr4)) thm (or42 () () (<-> (\/ (\/ ph ps) (\/ ch th)) (\/ (\/ ph ch) (\/ th ps))) (ph ps ch th or4 ps th orcom (\/ ph ch) orbi2i bitr)) thm (orordi () () (<-> (\/ ph (\/ ps ch)) (\/ (\/ ph ps) (\/ ph ch))) (ph oridm (\/ ps ch) orbi1i ph ph ps ch or4 bitr3)) thm (orordir () () (<-> (\/ (\/ ph ps) ch) (\/ (\/ ph ch) (\/ ps ch))) (ch oridm (\/ ph ps) orbi2i ph ps ch ch or4 bitr3)) thm (olc () () (-> ph (\/ ps ph)) (ph (-. ps) ax-1 orrd)) thm (pm2.07 () () (-> ph (\/ ph ph)) (ph ph olc)) thm (orc () () (-> ph (\/ ph ps)) (ph ps pm2.24 orrd)) thm (orci () ((orci.1 (-> (\/ ph ps) ch))) (-> ph ch) (ph ps orc orci.1 syl)) thm (olci () ((olci.1 (-> (\/ ph ps) ch))) (-> ps ch) (ps ph olc olci.1 syl)) thm (pm2.45 () () (-> (-. (\/ ph ps)) (-. ph)) (ph ps orc con3i)) thm (pm2.46 () () (-> (-. (\/ ph ps)) (-. ps)) (ps ph olc con3i)) thm (pm2.47 () () (-> (-. (\/ ph ps)) (\/ (-. ph) ps)) (ph ps pm2.45 (-. ph) ps orc syl)) thm (pm2.48 () () (-> (-. (\/ ph ps)) (\/ ph (-. ps))) (ph ps pm2.46 (-. ph) a1d orrd)) thm (pm2.49 () () (-> (-. (\/ ph ps)) (\/ (-. ph) (-. ps))) (ph ps pm2.46 (-. (-. ph)) a1d orrd)) thm (pm2.67 () () (-> (-> (\/ ph ps) ps) (-> ph ps)) (ph ps orc ps imim1i)) thm (pm3.2 () () (-> ph (-> ps (/\ ph ps))) (ph ps df-an biimpr expi)) thm (pm3.21 () () (-> ph (-> ps (/\ ps ph))) (ps ph pm3.2 com12)) thm (pm3.2i () ((pm3.2i.1 ph) (pm3.2i.2 ps)) (/\ ph ps) (pm3.2i.1 pm3.2i.2 ph ps pm3.2 mp2)) thm (pm3.37 () () (-> (-> (/\ ph ps) ch) (-> (/\ ph (-. ch)) (-. ps))) (ps ph pm3.21 ch imim1d com12 ph ch iman syl6ib con2d)) thm (pm3.43i () () (-> (-> ph ps) (-> (-> ph ch) (-> ph (/\ ps ch)))) (ps ch pm3.2 ph imim2i a2d)) thm (jca () ((jca.1 (-> ph ps)) (jca.2 (-> ph ch))) (-> ph (/\ ps ch)) (jca.1 jca.2 jc ps ch df-an sylibr)) thm (jcai () ((jcai.1 (-> ph ps)) (jcai.2 (-> ph (-> ps ch)))) (-> ph (/\ ps ch)) (jcai.1 jcai.1 jcai.2 mpd jca)) thm (jctl () ((jctl.1 ps)) (-> ph (/\ ps ph)) (jctl.1 ph a1i ph id jca)) thm (jctr () ((jctr.1 ps)) (-> ph (/\ ph ps)) (ph id jctr.1 ph a1i jca)) thm (jctil () ((jctil.1 (-> ph ps)) (jctil.2 ch)) (-> ph (/\ ch ps)) (jctil.2 ph a1i jctil.1 jca)) thm (jctir () ((jctir.1 (-> ph ps)) (jctir.2 ch)) (-> ph (/\ ps ch)) (jctir.1 jctir.2 ph a1i jca)) thm (ancl () () (-> (-> ph ps) (-> ph (/\ ph ps))) (ph ps pm3.2 a2i)) thm (ancr () () (-> (-> ph ps) (-> ph (/\ ps ph))) (ph ps pm3.21 a2i)) thm (ancli () ((ancli.1 (-> ph ps))) (-> ph (/\ ph ps)) (ph id ancli.1 jca)) thm (ancri () ((ancri.1 (-> ph ps))) (-> ph (/\ ps ph)) (ancri.1 ph id jca)) thm (ancld () ((ancld.1 (-> ph (-> ps ch)))) (-> ph (-> ps (/\ ps ch))) (ancld.1 ps ch ancl syl)) thm (ancrd () ((ancrd.1 (-> ph (-> ps ch)))) (-> ph (-> ps (/\ ch ps))) (ancrd.1 ps ch ancr syl)) thm (anc2l () () (-> (-> ph (-> ps ch)) (-> ph (-> ps (/\ ph ch)))) (ph ch pm3.2 ps imim2d a2i)) thm (anc2r () () (-> (-> ph (-> ps ch)) (-> ph (-> ps (/\ ch ph)))) (ph ch pm3.21 ps imim2d a2i)) thm (anc2li () ((anc2li.1 (-> ph (-> ps ch)))) (-> ph (-> ps (/\ ph ch))) (anc2li.1 ph ps ch anc2l ax-mp)) thm (anc2ri () ((anc2ri.1 (-> ph (-> ps ch)))) (-> ph (-> ps (/\ ch ph))) (anc2ri.1 ph ps ch anc2r ax-mp)) thm (anor () () (<-> (/\ ph ps) (-. (\/ (-. ph) (-. ps)))) (ph ps df-an ph (-. ps) imor negbii bitr)) thm (ianor () () (<-> (-. (/\ ph ps)) (\/ (-. ph) (-. ps))) (ph ps anor negbii (\/ (-. ph) (-. ps)) pm4.13 bitr4)) thm (ioran () () (<-> (-. (\/ ph ps)) (/\ (-. ph) (-. ps))) (ph pm4.13 ps pm4.13 orbi12i negbii (-. ph) (-. ps) anor bitr4)) thm (pm4.52 () () (<-> (/\ ph (-. ps)) (-. (\/ (-. ph) ps))) (ph (-. ps) anor ps pm4.13 (-. ph) orbi2i negbii bitr4)) thm (pm4.53 () () (<-> (-. (/\ ph (-. ps))) (\/ (-. ph) ps)) (ph ps pm4.52 bicon2i bicomi)) thm (pm4.54 () () (<-> (/\ (-. ph) ps) (-. (\/ ph (-. ps)))) ((-. ph) ps anor ph pm4.13 (-. ps) orbi1i negbii bitr4)) thm (pm4.55 () () (<-> (-. (/\ (-. ph) ps)) (\/ ph (-. ps))) (ph ps pm4.54 bicon2i bicomi)) thm (pm4.56 () () (<-> (/\ (-. ph) (-. ps)) (-. (\/ ph ps))) (ph ps ioran bicomi)) thm (oran () () (<-> (\/ ph ps) (-. (/\ (-. ph) (-. ps)))) ((\/ ph ps) pm4.13 ph ps ioran negbii bitr)) thm (pm4.57 () () (<-> (-. (/\ (-. ph) (-. ps))) (\/ ph ps)) (ph ps oran bicomi)) thm (pm3.1 () () (-> (/\ ph ps) (-. (\/ (-. ph) (-. ps)))) (ph ps anor biimp)) thm (pm3.11 () () (-> (-. (\/ (-. ph) (-. ps))) (/\ ph ps)) (ph ps anor biimpr)) thm (pm3.12 () () (\/ (\/ (-. ph) (-. ps)) (/\ ph ps)) (ph ps pm3.11 orri)) thm (pm3.13 () () (-> (-. (/\ ph ps)) (\/ (-. ph) (-. ps))) (ph ps pm3.11 con1i)) thm (pm3.14 () () (-> (\/ (-. ph) (-. ps)) (-. (/\ ph ps))) (ph ps pm3.1 con2i)) thm (pm3.26 () () (-> (/\ ph ps) ph) (ph ps df-an ph ps pm3.26im sylbi)) thm (pm3.26i () ((pm3.26i.1 (/\ ph ps))) ph (pm3.26i.1 ph ps pm3.26 ax-mp)) thm (pm3.26d () ((pm3.26d.1 (-> ph (/\ ps ch)))) (-> ph ps) (pm3.26d.1 ps ch pm3.26 syl)) thm (pm3.26bd () ((pm3.26bd.1 (<-> ph (/\ ps ch)))) (-> ph ps) (pm3.26bd.1 biimp pm3.26d)) thm (pm3.27 () () (-> (/\ ph ps) ps) (ph ps df-an ph ps pm3.27im sylbi)) thm (pm3.27i () ((pm3.27i.1 (/\ ph ps))) ps (pm3.27i.1 ph ps pm3.27 ax-mp)) thm (pm3.27d () ((pm3.27d.1 (-> ph (/\ ps ch)))) (-> ph ch) (pm3.27d.1 ps ch pm3.27 syl)) thm (pm3.27bd () ((pm3.27bd.1 (<-> ph (/\ ps ch)))) (-> ph ch) (pm3.27bd.1 biimp pm3.27d)) thm (pm3.41 () () (-> (-> ph ch) (-> (/\ ph ps) ch)) (ph ps pm3.26 ch imim1i)) thm (pm3.42 () () (-> (-> ps ch) (-> (/\ ph ps) ch)) (ph ps pm3.27 ch imim1i)) thm (anclb () () (<-> (-> ph ps) (-> ph (/\ ph ps))) (ph ps ancl ph ps pm3.27 ph imim2i impbi)) thm (ancrb () () (<-> (-> ph ps) (-> ph (/\ ps ph))) (ph ps ancr ps ph pm3.26 ph imim2i impbi)) thm (pm3.4 () () (-> (/\ ph ps) (-> ph ps)) (ph ps pm3.27 ph a1d)) thm (pm4.45im () () (<-> ph (/\ ph (-> ps ph))) (ph ps ax-1 ancli ph (-> ps ph) pm3.26 impbi)) thm (anim12i () ((anim12i.1 (-> ph ps)) (anim12i.2 (-> ch th))) (-> (/\ ph ch) (/\ ps th)) (ph ch pm3.26 anim12i.1 syl ph ch pm3.27 anim12i.2 syl jca)) thm (anim1i () ((anim1i.1 (-> ph ps))) (-> (/\ ph ch) (/\ ps ch)) (anim1i.1 ch id anim12i)) thm (anim2i () ((anim1i.1 (-> ph ps))) (-> (/\ ch ph) (/\ ch ps)) (ch id anim1i.1 anim12i)) thm (orim12i () ((orim12i.1 (-> ph ps)) (orim12i.2 (-> ch th))) (-> (\/ ph ch) (\/ ps th)) (orim12i.1 con3i orim12i.2 con3i anim12i con3i ph ch oran ps th oran 3imtr4)) thm (orim1i () ((orim1i.1 (-> ph ps))) (-> (\/ ph ch) (\/ ps ch)) (orim1i.1 ch id orim12i)) thm (orim2i () ((orim1i.1 (-> ph ps))) (-> (\/ ch ph) (\/ ch ps)) (ch id orim1i.1 orim12i)) thm (pm2.3 () () (-> (\/ ph (\/ ps ch)) (\/ ph (\/ ch ps))) (ps ch pm1.4 ph orim2i)) thm (jao () () (-> (-> ph ps) (-> (-> ch ps) (-> (\/ ph ch) ps))) (ph ps con3 (-. ps) (-. ph) (-. ch) pm3.43i ps (/\ (-. ph) (-. ch)) con1 syl6 ph ch oran bisyl7 ch ps con3 syl5 syl)) thm (jaoi () ((jaoi.1 (-> ph ps)) (jaoi.2 (-> ch ps))) (-> (\/ ph ch) ps) (jaoi.1 jaoi.2 ph ps ch jao mp2)) thm (pm2.41 () () (-> (\/ ps (\/ ph ps)) (\/ ph ps)) (ps ph olc (\/ ph ps) id jaoi)) thm (pm2.42 () () (-> (\/ (-. ph) (-> ph ps)) (-> ph ps)) (ph ps pm2.21 (-> ph ps) id jaoi)) thm (pm2.4 () () (-> (\/ ph (\/ ph ps)) (\/ ph ps)) (ph ps orc (\/ ph ps) id jaoi)) thm (pm4.44 () () (<-> ph (\/ ph (/\ ph ps))) (ph (/\ ph ps) orc ph id ph ps pm3.26 jaoi impbi)) thm (pm5.63 () () (<-> (\/ ph ps) (\/ ph (/\ (-. ph) ps))) (ph ps pm2.53 ancld orrd ph ps pm2.24 (-. ph) ps pm3.4 jaoi orrd impbi)) thm (impexp () () (<-> (-> (/\ ph ps) ch) (-> ph (-> ps ch))) (ph ps df-an ch imbi1i ph ps ch expt ph ps ch impt impbi bitr)) thm (pm3.3 () () (-> (-> (/\ ph ps) ch) (-> ph (-> ps ch))) (ph ps ch impexp biimp)) thm (pm3.31 () () (-> (-> ph (-> ps ch)) (-> (/\ ph ps) ch)) (ph ps ch impexp biimpr)) thm (imp () ((imp.1 (-> ph (-> ps ch)))) (-> (/\ ph ps) ch) (ph ps df-an imp.1 impi sylbi)) thm (impcom () ((imp.1 (-> ph (-> ps ch)))) (-> (/\ ps ph) ch) (imp.1 com12 imp)) thm (pm4.14 () () (<-> (-> (/\ ph ps) ch) (-> (/\ ph (-. ch)) (-. ps))) (ph ps ch impexp ph ps ch bi2.04 bitr ph ch iman ps imbi2i ps (/\ ph (-. ch)) bi2.03 3bitr)) thm (pm4.15 () () (<-> (-> (/\ ph ps) (-. ch)) (-> (/\ ps ch) (-. ph))) (ph ps (-. ch) impexp ps ch imnan ph imbi2i ph (/\ ps ch) bi2.03 3bitr)) thm (pm4.78 () () (<-> (\/ (-> ph ps) (-> ph ch)) (-> ph (\/ ps ch))) (ph (-. ps) (-> ph ch) impexp ph ps annim (-> ph ch) imbi1i (-. ps) ph ch bi2.04 ph imbi2i ph (-> (-. ps) ch) pm5.4 bitr 3bitr3 (-> ph ps) (-> ph ch) df-or ps ch df-or ph imbi2i 3bitr4)) thm (pm4.79 () () (<-> (\/ (-> ps ph) (-> ch ph)) (-> (/\ ps ch) ph)) ((-. ph) (-. ps) (-. ch) pm4.78 ps ch ianor (-. ph) imbi2i bitr4 ps ph pm4.1 ch ph pm4.1 orbi12i (/\ ps ch) ph pm4.1 3bitr4)) thm (pm4.87 () () (/\ (/\ (<-> (-> (/\ ph ps) ch) (-> ph (-> ps ch))) (<-> (-> ph (-> ps ch)) (-> ps (-> ph ch)))) (<-> (-> ps (-> ph ch)) (-> (/\ ps ph) ch))) (ph ps ch impexp ph ps ch bi2.04 pm3.2i ps ph ch pm3.31 ps ph ch pm3.3 impbi pm3.2i)) thm (pm3.33 () () (-> (/\ (-> ph ps) (-> ps ch)) (-> ph ch)) (ph ps ch imim1 imp)) thm (pm3.34 () () (-> (/\ (-> ps ch) (-> ph ps)) (-> ph ch)) (ps ch ph imim2 imp)) thm (pm3.35 () () (-> (/\ ph (-> ph ps)) ps) (ph ps pm2.27 imp)) thm (pm5.31 () () (-> (/\ ch (-> ph ps)) (-> ph (/\ ps ch))) (ch ps pm3.21 ph imim2d imp)) thm (imp3a () ((imp3.1 (-> ph (-> ps (-> ch th))))) (-> ph (-> (/\ ps ch) th)) (imp3.1 ps ch th impexp sylibr)) thm (imp31 () ((imp3.1 (-> ph (-> ps (-> ch th))))) (-> (/\ (/\ ph ps) ch) th) (imp3.1 imp imp)) thm (imp32 () ((imp3.1 (-> ph (-> ps (-> ch th))))) (-> (/\ ph (/\ ps ch)) th) (imp3.1 imp3a imp)) thm (imp4a () ((imp4.1 (-> ph (-> ps (-> ch (-> th ta)))))) (-> ph (-> ps (-> (/\ ch th) ta))) (imp4.1 ch th ta impexp syl6ibr)) thm (imp4b () ((imp4.1 (-> ph (-> ps (-> ch (-> th ta)))))) (-> (/\ ph ps) (-> (/\ ch th) ta)) (imp4.1 imp4a imp)) thm (imp4c () ((imp4.1 (-> ph (-> ps (-> ch (-> th ta)))))) (-> ph (-> (/\ (/\ ps ch) th) ta)) (imp4.1 imp3a imp3a)) thm (imp4d () ((imp4.1 (-> ph (-> ps (-> ch (-> th ta)))))) (-> ph (-> (/\ ps (/\ ch th)) ta)) (imp4.1 imp4a imp3a)) thm (imp41 () ((imp4.1 (-> ph (-> ps (-> ch (-> th ta)))))) (-> (/\ (/\ (/\ ph ps) ch) th) ta) (imp4.1 imp imp31)) thm (imp42 () ((imp4.1 (-> ph (-> ps (-> ch (-> th ta)))))) (-> (/\ (/\ ph (/\ ps ch)) th) ta) (imp4.1 imp32 imp)) thm (imp43 () ((imp4.1 (-> ph (-> ps (-> ch (-> th ta)))))) (-> (/\ (/\ ph ps) (/\ ch th)) ta) (imp4.1 imp4b imp)) thm (imp44 () ((imp4.1 (-> ph (-> ps (-> ch (-> th ta)))))) (-> (/\ ph (/\ (/\ ps ch) th)) ta) (imp4.1 imp4c imp)) thm (imp45 () ((imp4.1 (-> ph (-> ps (-> ch (-> th ta)))))) (-> (/\ ph (/\ ps (/\ ch th))) ta) (imp4.1 imp4d imp)) thm (exp () ((exp.1 (-> (/\ ph ps) ch))) (-> ph (-> ps ch)) (ph ps df-an exp.1 sylbir expi)) thm (expcom () ((exp.1 (-> (/\ ph ps) ch))) (-> ps (-> ph ch)) (exp.1 exp com12)) thm (exp3a () ((exp3a.1 (-> ph (-> (/\ ps ch) th)))) (-> ph (-> ps (-> ch th))) (exp3a.1 ps ch th impexp sylib)) thm (exp31 () ((exp31.1 (-> (/\ (/\ ph ps) ch) th))) (-> ph (-> ps (-> ch th))) (exp31.1 exp exp)) thm (exp32 () ((exp32.1 (-> (/\ ph (/\ ps ch)) th))) (-> ph (-> ps (-> ch th))) (exp32.1 exp exp3a)) thm (exp4a () ((exp4a.1 (-> ph (-> ps (-> (/\ ch th) ta))))) (-> ph (-> ps (-> ch (-> th ta)))) (exp4a.1 ch th ta impexp syl6ib)) thm (exp4b () ((exp4b.1 (-> (/\ ph ps) (-> (/\ ch th) ta)))) (-> ph (-> ps (-> ch (-> th ta)))) (exp4b.1 exp3a exp)) thm (exp4c () ((exp4c.1 (-> ph (-> (/\ (/\ ps ch) th) ta)))) (-> ph (-> ps (-> ch (-> th ta)))) (exp4c.1 exp3a exp3a)) thm (exp4d () ((exp4d.1 (-> ph (-> (/\ ps (/\ ch th)) ta)))) (-> ph (-> ps (-> ch (-> th ta)))) (exp4d.1 exp3a exp4a)) thm (exp41 () ((exp41.1 (-> (/\ (/\ (/\ ph ps) ch) th) ta))) (-> ph (-> ps (-> ch (-> th ta)))) (exp41.1 exp exp31)) thm (exp42 () ((exp42.1 (-> (/\ (/\ ph (/\ ps ch)) th) ta))) (-> ph (-> ps (-> ch (-> th ta)))) (exp42.1 exp31 exp3a)) thm (exp43 () ((exp43.1 (-> (/\ (/\ ph ps) (/\ ch th)) ta))) (-> ph (-> ps (-> ch (-> th ta)))) (exp43.1 exp exp4b)) thm (exp44 () ((exp44.1 (-> (/\ ph (/\ (/\ ps ch) th)) ta))) (-> ph (-> ps (-> ch (-> th ta)))) (exp44.1 exp32 exp3a)) thm (exp45 () ((exp45.1 (-> (/\ ph (/\ ps (/\ ch th))) ta))) (-> ph (-> ps (-> ch (-> th ta)))) (exp45.1 exp32 exp4a)) thm (impac () ((impac.1 (-> ph (-> ps ch)))) (-> (/\ ph ps) (/\ ch ps)) (impac.1 ancrd imp)) thm (adantl () ((adantl.1 (-> ph ps))) (-> (/\ ch ph) ps) (adantl.1 ch a1i imp)) thm (adantr () ((adantr.1 (-> ph ps))) (-> (/\ ph ch) ps) (adantr.1 ch a1d imp)) thm (adantld () ((adantld.1 (-> ph (-> ps ch)))) (-> ph (-> (/\ th ps) ch)) (adantld.1 th a1d imp3a)) thm (adantrd () ((adantrd.1 (-> ph (-> ps ch)))) (-> ph (-> (/\ ps th) ch)) (adantrd.1 ps th pm3.26 syl5)) thm (adantll () ((adant2.1 (-> (/\ ph ps) ch))) (-> (/\ (/\ th ph) ps) ch) (adant2.1 exp th adantl imp)) thm (adantlr () ((adant2.1 (-> (/\ ph ps) ch))) (-> (/\ (/\ ph th) ps) ch) (adant2.1 exp th adantr imp)) thm (adantrl () ((adant2.1 (-> (/\ ph ps) ch))) (-> (/\ ph (/\ th ps)) ch) (adant2.1 exp th adantld imp)) thm (adantrr () ((adant2.1 (-> (/\ ph ps) ch))) (-> (/\ ph (/\ ps th)) ch) (adant2.1 exp th adantrd imp)) thm (adantlll () ((adantl2.1 (-> (/\ (/\ ph ps) ch) th))) (-> (/\ (/\ (/\ ta ph) ps) ch) th) (adantl2.1 exp31 ta a1i imp41)) thm (adantllr () ((adantl2.1 (-> (/\ (/\ ph ps) ch) th))) (-> (/\ (/\ (/\ ph ta) ps) ch) th) (adantl2.1 exp31 ta a1d imp41)) thm (adantlrl () ((adantl2.1 (-> (/\ (/\ ph ps) ch) th))) (-> (/\ (/\ ph (/\ ta ps)) ch) th) (adantl2.1 exp31 ta a1d imp42)) thm (adantlrr () ((adantl2.1 (-> (/\ (/\ ph ps) ch) th))) (-> (/\ (/\ ph (/\ ps ta)) ch) th) (adantl2.1 exp31 ta a1dd imp42)) thm (adantrll () ((adantr2.1 (-> (/\ ph (/\ ps ch)) th))) (-> (/\ ph (/\ (/\ ta ps) ch)) th) (adantr2.1 exp32 ta a1d imp44)) thm (adantrlr () ((adantr2.1 (-> (/\ ph (/\ ps ch)) th))) (-> (/\ ph (/\ (/\ ps ta) ch)) th) (adantr2.1 exp32 ta a1dd imp44)) thm (adantrrl () ((adantr2.1 (-> (/\ ph (/\ ps ch)) th))) (-> (/\ ph (/\ ps (/\ ta ch))) th) (adantr2.1 exp32 ta a1dd imp45)) thm (adantrrr () ((adantr2.1 (-> (/\ ph (/\ ps ch)) th))) (-> (/\ ph (/\ ps (/\ ch ta))) th) (adantr2.1 ta a1d exp32 imp45)) thm (ad2antll () ((ad2ant.1 (-> ph ps))) (-> (/\ (/\ ph ch) th) ps) (ad2ant.1 ch adantr th adantr)) thm (ad2antlr () ((ad2ant.1 (-> ph ps))) (-> (/\ (/\ ch ph) th) ps) (ad2ant.1 ch adantl th adantr)) thm (ad2antrl () ((ad2ant.1 (-> ph ps))) (-> (/\ ch (/\ ph th)) ps) (ad2ant.1 th adantr ch adantl)) thm (ad2antrr () ((ad2ant.1 (-> ph ps))) (-> (/\ ch (/\ th ph)) ps) (ad2ant.1 th adantl ch adantl)) thm (biimpa () ((biimpa.1 (-> ph (<-> ps ch)))) (-> (/\ ph ps) ch) (biimpa.1 biimpd imp)) thm (biimpar () ((biimpa.1 (-> ph (<-> ps ch)))) (-> (/\ ph ch) ps) (biimpa.1 biimprd imp)) thm (biimpac () ((biimpa.1 (-> ph (<-> ps ch)))) (-> (/\ ps ph) ch) (biimpa.1 biimpcd imp)) thm (biimparc () ((biimpa.1 (-> ph (<-> ps ch)))) (-> (/\ ch ph) ps) (biimpa.1 biimprcd imp)) thm (jaob () () (<-> (-> (\/ ph ch) ps) (/\ (-> ph ps) (-> ch ps))) (ph ch orc ps imim1i ch ph olc ps imim1i jca ph ps ch jao imp impbi)) thm (pm4.77 () () (<-> (/\ (-> ps ph) (-> ch ph)) (-> (\/ ps ch) ph)) (ps ch ph jaob bicomi)) thm (jaod () ((jaod.1 (-> ph (-> ps ch))) (jaod.2 (-> ph (-> th ch)))) (-> ph (-> (\/ ps th) ch)) (ps ch th jao jaod.1 jaod.2 sylc)) thm (jaodan () ((jaodan.1 (-> (/\ ph ps) ch)) (jaodan.2 (-> (/\ ph th) ch))) (-> (/\ ph (\/ ps th)) ch) (jaodan.1 exp jaodan.2 exp jaod imp)) thm (jaao () ((jaao.1 (-> ph (-> ps ch))) (jaao.2 (-> th (-> ta ch)))) (-> (/\ ph th) (-> (\/ ps ta) ch)) (jaao.1 th adantr jaao.2 ph adantl jaod)) thm (pm2.63 () () (-> (\/ ph ps) (-> (\/ (-. ph) ps) ps)) (ph ps pm2.53 (\/ ph ps) ps idd jaod)) thm (pm2.64 () () (-> (\/ ph ps) (-> (\/ ph (-. ps)) ph)) (ph (\/ ph ps) ax-1 ps ph orel2 jaoi com12)) thm (pm3.44 () () (-> (/\ (-> ps ph) (-> ch ph)) (-> (\/ ps ch) ph)) (ps ch ph jaob biimpr)) thm (pm4.43 () () (<-> ph (/\ (\/ ph ps) (\/ ph (-. ps)))) (ph ps orc ph (-. ps) orc jca ph ps pm2.64 imp impbi)) thm (anidm () () (<-> (/\ ph ph) ph) (ph ph pm3.26 ph ph pm3.2 pm2.43i impbi)) thm (pm4.24 () () (<-> ph (/\ ph ph)) (ph anidm bicomi)) thm (anidms () ((anidms.1 (-> (/\ ph ph) ps))) (-> ph ps) (anidms.1 exp pm2.43i)) thm (ancom () () (<-> (/\ ph ps) (/\ ps ph)) (ph ps pm3.27 ph ps pm3.26 jca ps ph pm3.27 ps ph pm3.26 jca impbi)) thm (ancoms () ((ancoms.1 (-> (/\ ph ps) ch))) (-> (/\ ps ph) ch) (ps ph ancom ancoms.1 sylbi)) thm (ancomsd () ((ancomsd.1 (-> ph (-> (/\ ps ch) th)))) (-> ph (-> (/\ ch ps) th)) (ancomsd.1 ch ps ancom syl5ib)) thm (pm3.22 () () (-> (/\ ph ps) (/\ ps ph)) (ph ps ancom biimp)) thm (anass () () (<-> (/\ (/\ ph ps) ch) (/\ ph (/\ ps ch))) (ph ps (-. ch) impexp ps ch imnan ph imbi2i bitr negbii (/\ ph ps) ch df-an ph (/\ ps ch) df-an 3bitr4)) thm (anasss () ((anasss.1 (-> (/\ (/\ ph ps) ch) th))) (-> (/\ ph (/\ ps ch)) th) (anasss.1 exp31 imp32)) thm (anassrs () ((anassrs.1 (-> (/\ ph (/\ ps ch)) th))) (-> (/\ (/\ ph ps) ch) th) (anassrs.1 exp32 imp31)) thm (imdistan () () (<-> (-> ph (-> ps ch)) (-> (/\ ph ps) (/\ ph ch))) (ph ps ch anc2l imp3a ph ch pm3.27 (/\ ph ps) imim2i exp3a impbi)) thm (imdistani () ((imdistani.1 (-> ph (-> ps ch)))) (-> (/\ ph ps) (/\ ph ch)) (imdistani.1 anc2li imp)) thm (imdistanri () ((imdistanri.1 (-> ph (-> ps ch)))) (-> (/\ ps ph) (/\ ch ph)) (imdistanri.1 com12 impac)) thm (imdistand () ((imdistand.1 (-> ph (-> ps (-> ch th))))) (-> ph (-> (/\ ps ch) (/\ ps th))) (imdistand.1 ps ch th imdistan sylib)) thm (pm5.3 () () (<-> (-> (/\ ph ps) ch) (-> (/\ ph ps) (/\ ph ch))) (ph ps ch pm3.3 imdistand ph ch pm3.27 (/\ ph ps) imim2i impbi)) thm (pm5.61 () () (<-> (/\ (\/ ph ps) (-. ps)) (/\ ph (-. ps))) (ps ph orel2 imdistanri ph ps orc (-. ps) anim1i impbi)) thm (sylan () ((sylan.1 (-> (/\ ph ps) ch)) (sylan.2 (-> th ph))) (-> (/\ th ps) ch) (sylan.2 sylan.1 exp syl imp)) thm (sylanb () ((sylan.1 (-> (/\ ph ps) ch)) (sylanb.2 (<-> th ph))) (-> (/\ th ps) ch) (sylan.1 sylanb.2 biimp sylan)) thm (sylanbr () ((sylan.1 (-> (/\ ph ps) ch)) (sylanbr.2 (<-> ph th))) (-> (/\ th ps) ch) (sylan.1 sylanbr.2 biimpr sylan)) thm (sylan2 () ((sylan.1 (-> (/\ ph ps) ch)) (sylan2.2 (-> th ps))) (-> (/\ ph th) ch) (sylan.1 exp sylan2.2 syl5 imp)) thm (sylan2b () ((sylan.1 (-> (/\ ph ps) ch)) (sylan2b.2 (<-> th ps))) (-> (/\ ph th) ch) (sylan.1 sylan2b.2 biimp sylan2)) thm (sylan2br () ((sylan.1 (-> (/\ ph ps) ch)) (sylan2br.2 (<-> ps th))) (-> (/\ ph th) ch) (sylan.1 sylan2br.2 biimpr sylan2)) thm (syl2an () ((sylan.1 (-> (/\ ph ps) ch)) (syl2an.2 (-> th ph)) (syl2an.3 (-> ta ps))) (-> (/\ th ta) ch) (sylan.1 syl2an.2 sylan syl2an.3 sylan2)) thm (syl2anb () ((sylan.1 (-> (/\ ph ps) ch)) (syl2anb.2 (<-> th ph)) (syl2anb.3 (<-> ta ps))) (-> (/\ th ta) ch) (sylan.1 syl2anb.2 sylanb syl2anb.3 sylan2b)) thm (syl2anbr () ((sylan.1 (-> (/\ ph ps) ch)) (syl2anbr.2 (<-> ph th)) (syl2anbr.3 (<-> ps ta))) (-> (/\ th ta) ch) (sylan.1 syl2anbr.2 sylanbr syl2anbr.3 sylan2br)) thm (syland () ((syland.1 (-> ph (-> (/\ ps ch) th))) (syland.2 (-> ph (-> ta ps)))) (-> ph (-> (/\ ta ch) th)) (syland.2 syland.1 exp3a syld imp3a)) thm (sylan2d () ((sylan2d.1 (-> ph (-> (/\ ps ch) th))) (sylan2d.2 (-> ph (-> ta ch)))) (-> ph (-> (/\ ps ta) th)) (sylan2d.1 ancomsd sylan2d.2 syland ancomsd)) var (wff et) thm (syl2and () ((syl2and.1 (-> ph (-> (/\ ps ch) th))) (syl2and.2 (-> ph (-> ta ps))) (syl2and.3 (-> ph (-> et ch)))) (-> ph (-> (/\ ta et) th)) (syl2and.1 syl2and.3 sylan2d syl2and.2 syland)) thm (sylanl1 () ((sylanl1.1 (-> (/\ (/\ ph ps) ch) th)) (sylanl1.2 (-> ta ph))) (-> (/\ (/\ ta ps) ch) th) (sylanl1.1 sylanl1.2 ps anim1i sylan)) thm (sylanl2 () ((sylanl2.1 (-> (/\ (/\ ph ps) ch) th)) (sylanl2.2 (-> ta ps))) (-> (/\ (/\ ph ta) ch) th) (sylanl2.1 sylanl2.2 ph anim2i sylan)) thm (sylanr1 () ((sylanr1.1 (-> (/\ ph (/\ ps ch)) th)) (sylanr1.2 (-> ta ps))) (-> (/\ ph (/\ ta ch)) th) (sylanr1.1 sylanr1.2 ch anim1i sylan2)) thm (sylanr2 () ((sylanr2.1 (-> (/\ ph (/\ ps ch)) th)) (sylanr2.2 (-> ta ch))) (-> (/\ ph (/\ ps ta)) th) (sylanr2.1 sylanr2.2 ps anim2i sylan2)) thm (sylani () ((sylani.1 (-> ph (-> (/\ ps ch) th))) (sylani.2 (-> ta ps))) (-> ph (-> (/\ ta ch) th)) (sylani.1 sylani.2 ph a1i syland)) thm (sylan2i () ((sylan2i.1 (-> ph (-> (/\ ps ch) th))) (sylan2i.2 (-> ta ch))) (-> ph (-> (/\ ps ta) th)) (sylan2i.1 sylan2i.2 ph a1i sylan2d)) thm (syl2ani () ((syl2ani.1 (-> ph (-> (/\ ps ch) th))) (syl2ani.2 (-> ta ps)) (syl2ani.3 (-> et ch))) (-> ph (-> (/\ ta et) th)) (syl2ani.1 syl2ani.3 sylan2i syl2ani.2 sylani)) thm (syldan () ((syldan.1 (-> (/\ ph ps) ch)) (syldan.2 (-> (/\ ph ch) th))) (-> (/\ ph ps) th) (syldan.1 exp syldan.2 exp syld imp)) thm (sylan9 () ((sylan9.1 (-> ph (-> ps ch))) (sylan9.2 (-> th (-> ch ta)))) (-> (/\ ph th) (-> ps ta)) (sylan9.1 th adantr sylan9.2 ph adantl syld)) thm (sylan9r () ((sylan9r.1 (-> ph (-> ps ch))) (sylan9r.2 (-> th (-> ch ta)))) (-> (/\ th ph) (-> ps ta)) (sylan9r.1 sylan9r.2 syl9r imp)) thm (sylanc () ((sylanc.1 (-> (/\ ph ps) ch)) (sylanc.2 (-> th ph)) (sylanc.3 (-> th ps))) (-> th ch) (sylanc.1 exp sylanc.2 sylanc.3 sylc)) thm (sylancb () ((sylancb.1 (-> (/\ ph ps) ch)) (sylancb.2 (<-> th ph)) (sylancb.3 (<-> th ps))) (-> th ch) (sylancb.1 sylancb.2 sylancb.3 syl2anb anidms)) thm (sylancbr () ((sylancbr.1 (-> (/\ ph ps) ch)) (sylancbr.2 (<-> ph th)) (sylancbr.3 (<-> ps th))) (-> th ch) (sylancbr.1 sylancbr.2 sylancbr.3 syl2anbr anidms)) thm (pm2.61an1 () ((pm2.61an1.1 (-> (/\ ph ps) ch)) (pm2.61an1.2 (-> (/\ (-. ph) ps) ch))) (-> ps ch) (pm2.61an1.1 exp pm2.61an1.2 exp pm2.61i)) thm (pm2.61an2 () ((pm2.61an2.1 (-> (/\ ph ps) ch)) (pm2.61an2.2 (-> (/\ ph (-. ps)) ch))) (-> ph ch) (pm2.61an2.1 exp pm2.61an2.2 exp pm2.61d)) thm (abai () () (<-> (/\ ph ps) (/\ ph (-> ph ps))) (ph ps pm3.26 ph ps pm3.4 jca ph (-> ph ps) pm3.26 ph ps pm3.35 jca impbi)) thm (anbi2i () ((bi.aa (<-> ph ps))) (<-> (/\ ch ph) (/\ ch ps)) (bi.aa biimp ch anim2i bi.aa biimpr ch anim2i impbi)) thm (anbi1i () ((bi.aa (<-> ph ps))) (<-> (/\ ph ch) (/\ ps ch)) (ph ch ancom bi.aa ch anbi2i ch ps ancom 3bitr)) thm (anbi12i () ((bi2an.1 (<-> ph ps)) (bi2an.2 (<-> ch th))) (<-> (/\ ph ch) (/\ ps th)) (bi2an.1 ch anbi1i bi2an.2 ps anbi2i bitr)) thm (pm5.53 () () (<-> (-> (\/ (\/ ph ps) ch) th) (/\ (/\ (-> ph th) (-> ps th)) (-> ch th))) ((\/ ph ps) ch th jaob ph ps th jaob (-> ch th) anbi1i bitr)) thm (an12 () () (<-> (/\ ph (/\ ps ch)) (/\ ps (/\ ph ch))) (ph ps ancom ch anbi1i ph ps ch anass ps ph ch anass 3bitr3)) thm (an23 () () (<-> (/\ (/\ ph ps) ch) (/\ (/\ ph ch) ps)) (ps ch ancom ph anbi2i ph ps ch anass ph ch ps anass 3bitr4)) thm (an1s () ((an1s.1 (-> (/\ ph (/\ ps ch)) th))) (-> (/\ ps (/\ ph ch)) th) (ps ph ch an12 an1s.1 sylbi)) thm (an1rs () ((an1rs.1 (-> (/\ (/\ ph ps) ch) th))) (-> (/\ (/\ ph ch) ps) th) (ph ch ps an23 an1rs.1 sylbi)) thm (anabs1 () () (<-> (/\ (/\ ph ps) ph) (/\ ph ps)) ((/\ ph ps) ph pm3.26 (/\ ph ps) id ph ps pm3.26 jca impbi)) thm (anabs5 () () (<-> (/\ ph (/\ ph ps)) (/\ ph ps)) ((/\ ph ps) ph ancom ph ps anabs1 bitr3)) thm (anabs7 () () (<-> (/\ ps (/\ ph ps)) (/\ ph ps)) (ps (/\ ph ps) pm3.27 ph ps pm3.27 (/\ ph ps) id jca impbi)) thm (anabsi5 () ((anabsi5.1 (-> ph (-> (/\ ph ps) ch)))) (-> (/\ ph ps) ch) (anabsi5.1 ps adantr pm2.43i)) thm (anabsi6 () ((anabsi6.1 (-> ph (-> (/\ ps ph) ch)))) (-> (/\ ph ps) ch) (anabsi6.1 ancomsd anabsi5)) thm (anabsi7 () ((anabsi7.1 (-> ps (-> (/\ ph ps) ch)))) (-> (/\ ph ps) ch) (anabsi7.1 exp3a pm2.43b imp)) thm (anabsi8 () ((anabsi8.1 (-> ps (-> (/\ ps ph) ch)))) (-> (/\ ph ps) ch) (anabsi8.1 anabsi5 ancoms)) thm (anabss1 () ((anabss1.1 (-> (/\ (/\ ph ps) ph) ch))) (-> (/\ ph ps) ch) (anabss1.1 ps adantrr anidms)) thm (anabss3 () ((anabss3.1 (-> (/\ (/\ ph ps) ps) ch))) (-> (/\ ph ps) ch) (anabss3.1 ph adantrl anidms)) thm (anabss4 () ((anabss4.1 (-> (/\ (/\ ps ph) ps) ch))) (-> (/\ ph ps) ch) (anabss4.1 anabss1 ancoms)) thm (anabss5 () ((anabss5.1 (-> (/\ ph (/\ ph ps)) ch))) (-> (/\ ph ps) ch) (anabss5.1 ps adantlr anidms)) thm (anabss7 () ((anabss7.1 (-> (/\ ps (/\ ph ps)) ch))) (-> (/\ ph ps) ch) (anabss7.1 exp anabsi7)) thm (anabsan () ((anabsan.1 (-> (/\ (/\ ph ph) ps) ch))) (-> (/\ ph ps) ch) (anabsan.1 an1rs anabss1)) thm (anabsan2 () ((anabsan2.1 (-> (/\ ph (/\ ps ps)) ch))) (-> (/\ ph ps) ch) (anabsan2.1 anassrs anabss3)) thm (an4 () () (<-> (/\ (/\ ph ps) (/\ ch th)) (/\ (/\ ph ch) (/\ ps th))) (ps ch th an12 ph anbi2i ph ps (/\ ch th) anass ph ch (/\ ps th) anass 3bitr4)) thm (an42 () () (<-> (/\ (/\ ph ps) (/\ ch th)) (/\ (/\ ph ch) (/\ th ps))) (ph ps ch th an4 ps th ancom (/\ ph ch) anbi2i bitr)) thm (an4s () ((an4s.1 (-> (/\ (/\ ph ps) (/\ ch th)) ta))) (-> (/\ (/\ ph ch) (/\ ps th)) ta) (ph ch ps th an4 an4s.1 sylbi)) thm (an42s () ((an41r3s.1 (-> (/\ (/\ ph ps) (/\ ch th)) ta))) (-> (/\ (/\ ph ch) (/\ th ps)) ta) (ph ps ch th an42 an41r3s.1 sylbir)) thm (anandi () () (<-> (/\ ph (/\ ps ch)) (/\ (/\ ph ps) (/\ ph ch))) (ph anidm (/\ ps ch) anbi1i ph ph ps ch an4 bitr3)) thm (anandir () () (<-> (/\ (/\ ph ps) ch) (/\ (/\ ph ch) (/\ ps ch))) (ch anidm (/\ ph ps) anbi2i ph ps ch ch an4 bitr3)) thm (anandis () ((anandis.1 (-> (/\ (/\ ph ps) (/\ ph ch)) ta))) (-> (/\ ph (/\ ps ch)) ta) (anandis.1 an4s anabsan)) thm (anandirs () ((anandirs.1 (-> (/\ (/\ ph ch) (/\ ps ch)) ta))) (-> (/\ (/\ ph ps) ch) ta) (anandirs.1 an4s anabsan2)) thm (bi () () (<-> (<-> ph ps) (/\ (-> ph ps) (-> ps ph))) (ph ps bii (-> ph ps) (-> ps ph) df-an bitr4)) thm (impbid () ((impbid.1 (-> ph (-> ps ch))) (impbid.2 (-> ph (-> ch ps)))) (-> ph (<-> ps ch)) (impbid.1 impbid.2 jca ps ch bi sylibr)) thm (bicom () () (<-> (<-> ph ps) (<-> ps ph)) ((-> ph ps) (-> ps ph) ancom ph ps bi ps ph bi 3bitr4)) thm (bicomd () ((bicomd.1 (-> ph (<-> ps ch)))) (-> ph (<-> ch ps)) (bicomd.1 ps ch bicom sylib)) thm (pm4.11 () () (<-> (<-> ph ps) (<-> (-. ph) (-. ps))) (ph ps pm4.1 ps ph pm4.1 anbi12i ph ps bi (-. ps) (-. ph) bi 3bitr4 (-. ps) (-. ph) bicom bitr)) thm (bicon4i () ((bicon4.1 (<-> (-. ph) (-. ps)))) (<-> ph ps) (bicon4.1 ph ps pm4.11 mpbir)) thm (bicon4d () ((bicon4d.1 (-> ph (<-> (-. ps) (-. ch))))) (-> ph (<-> ps ch)) (bicon4d.1 ps ch pm4.11 sylibr)) thm (bicon2 () () (<-> (<-> ph (-. ps)) (<-> ps (-. ph))) (ph ps bi2.03 ps ph bi2.15 anbi12i ph (-. ps) bi ps (-. ph) bi 3bitr4)) thm (bicon2d () ((bicon2d.1 (-> ph (<-> ps (-. ch))))) (-> ph (<-> ch (-. ps))) (bicon2d.1 ch ps bicon2 sylibr)) thm (bicon1d () ((bicon1d.1 (-> ph (<-> (-. ps) ch)))) (-> ph (<-> (-. ch) ps)) (bicon1d.1 bicomd bicon2d bicomd)) thm (bitrd () ((bitrd.1 (-> ph (<-> ps ch))) (bitrd.2 (-> ph (<-> ch th)))) (-> ph (<-> ps th)) (bitrd.1 biimpd bitrd.2 sylibd bitrd.2 biimprd bitrd.1 sylibrd impbid)) thm (bitr2d () ((bitr2d.1 (-> ph (<-> ps ch))) (bitr2d.2 (-> ph (<-> ch th)))) (-> ph (<-> th ps)) (bitr2d.1 bitr2d.2 bitrd bicomd)) thm (bitr3d () ((bitr3d.1 (-> ph (<-> ps ch))) (bitr3d.2 (-> ph (<-> ps th)))) (-> ph (<-> ch th)) (bitr3d.1 bicomd bitr3d.2 bitrd)) thm (bitr4d () ((bitr4d.1 (-> ph (<-> ps ch))) (bitr4d.2 (-> ph (<-> th ch)))) (-> ph (<-> ps th)) (bitr4d.1 bitr4d.2 bicomd bitrd)) thm (syl5bb () ((syl5bb.1 (-> ph (<-> ps ch))) (syl5bb.2 (<-> th ps))) (-> ph (<-> th ch)) (syl5bb.2 ph a1i syl5bb.1 bitrd)) thm (syl5rbb () ((syl5rbb.1 (-> ph (<-> ps ch))) (syl5rbb.2 (<-> th ps))) (-> ph (<-> ch th)) (syl5rbb.1 syl5rbb.2 syl5bb bicomd)) thm (syl5bbr () ((syl5bbr.1 (-> ph (<-> ps ch))) (syl5bbr.2 (<-> ps th))) (-> ph (<-> th ch)) (syl5bbr.1 syl5bbr.2 bicomi syl5bb)) thm (syl5rbbr () ((syl5rbbr.1 (-> ph (<-> ps ch))) (syl5rbbr.2 (<-> ps th))) (-> ph (<-> ch th)) (syl5rbbr.1 syl5rbbr.2 bicomi syl5rbb)) thm (syl6bb () ((syl6bb.1 (-> ph (<-> ps ch))) (syl6bb.2 (<-> ch th))) (-> ph (<-> ps th)) (syl6bb.1 syl6bb.2 ph a1i bitrd)) thm (syl6rbb () ((syl6rbb.1 (-> ph (<-> ps ch))) (syl6rbb.2 (<-> ch th))) (-> ph (<-> th ps)) (syl6rbb.1 syl6rbb.2 syl6bb bicomd)) thm (syl6bbr () ((syl6bbr.1 (-> ph (<-> ps ch))) (syl6bbr.2 (<-> th ch))) (-> ph (<-> ps th)) (syl6bbr.1 syl6bbr.2 bicomi syl6bb)) thm (syl6rbbr () ((syl6rbbr.1 (-> ph (<-> ps ch))) (syl6rbbr.2 (<-> th ch))) (-> ph (<-> th ps)) (syl6rbbr.1 syl6rbbr.2 bicomi syl6rbb)) thm (sylan9bb () ((sylan9bb.1 (-> ph (<-> ps ch))) (sylan9bb.2 (-> th (<-> ch ta)))) (-> (/\ ph th) (<-> ps ta)) (sylan9bb.1 th adantr sylan9bb.2 ph adantl bitrd)) thm (sylan9bbr () ((sylan9bbr.1 (-> ph (<-> ps ch))) (sylan9bbr.2 (-> th (<-> ch ta)))) (-> (/\ th ph) (<-> ps ta)) (sylan9bbr.1 sylan9bbr.2 sylan9bb ancoms)) thm (3imtr3d () ((3imtr3d.1 (-> ph (-> ps ch))) (3imtr3d.2 (-> ph (<-> ps th))) (3imtr3d.3 (-> ph (<-> ch ta)))) (-> ph (-> th ta)) (3imtr3d.2 3imtr3d.1 3imtr3d.3 sylibd sylbird)) thm (3imtr4d () ((3imtr4d.1 (-> ph (-> ps ch))) (3imtr4d.2 (-> ph (<-> th ps))) (3imtr4d.3 (-> ph (<-> ta ch)))) (-> ph (-> th ta)) (3imtr4d.2 3imtr4d.1 3imtr4d.3 sylibrd sylbid)) thm (3bitrd () ((3bitrd.1 (-> ph (<-> ps ch))) (3bitrd.2 (-> ph (<-> ch th))) (3bitrd.3 (-> ph (<-> th ta)))) (-> ph (<-> ps ta)) (3bitrd.1 3bitrd.2 bitrd 3bitrd.3 bitrd)) thm (3bitr3d () ((3bitr3d.1 (-> ph (<-> ps ch))) (3bitr3d.2 (-> ph (<-> ps th))) (3bitr3d.3 (-> ph (<-> ch ta)))) (-> ph (<-> th ta)) (3bitr3d.2 3bitr3d.1 bitr3d 3bitr3d.3 bitrd)) thm (3bitr4d () ((3bitr4d.1 (-> ph (<-> ps ch))) (3bitr4d.2 (-> ph (<-> th ps))) (3bitr4d.3 (-> ph (<-> ta ch)))) (-> ph (<-> th ta)) (3bitr4d.2 3bitr4d.1 3bitr4d.3 bitr4d bitrd)) thm (3imtr3g () ((3imtr3g.1 (-> ph (-> ps ch))) (3imtr3g.2 (<-> ps th)) (3imtr3g.3 (<-> ch ta))) (-> ph (-> th ta)) (3imtr3g.1 imp 3imtr3g.2 ph anbi2i 3imtr3g.3 3imtr3 exp)) thm (3imtr4g () ((3imtr4g.1 (-> ph (-> ps ch))) (3imtr4g.2 (<-> th ps)) (3imtr4g.3 (<-> ta ch))) (-> ph (-> th ta)) (3imtr4g.1 3imtr4g.2 bicomi 3imtr4g.3 bicomi 3imtr3g)) thm (3bitr3g () ((3bitr3g.1 (-> ph (<-> ps ch))) (3bitr3g.2 (<-> ps th)) (3bitr3g.3 (<-> ch ta))) (-> ph (<-> th ta)) (3bitr3g.1 3bitr3g.2 syl5bbr 3bitr3g.3 syl6bb)) thm (3bitr4g () ((3bitr4g.1 (-> ph (<-> ps ch))) (3bitr4g.2 (<-> th ps)) (3bitr4g.3 (<-> ta ch))) (-> ph (<-> th ta)) (3bitr4g.1 3bitr4g.2 syl5bb 3bitr4g.3 syl6bbr)) thm (prth () () (-> (/\ (-> ph ps) (-> ch th)) (-> (/\ ph ch) (/\ ps th))) (ps th pm3.2 ch imim2d ph imim2i com23 imp4b)) thm (pm3.48 () () (-> (/\ (-> ph ps) (-> ch th)) (-> (\/ ph ch) (\/ ps th))) ((-> ph ps) (-> ch th) pm3.26 con3d (-> ph ps) (-> ch th) pm3.27 imim12d ph ch df-or ps th df-or 3imtr4g)) thm (anim12d () ((anim12d.1 (-> ph (-> ps ch))) (anim12d.2 (-> ph (-> th ta)))) (-> ph (-> (/\ ps th) (/\ ch ta))) (ps ch th ta prth anim12d.1 anim12d.2 sylanc)) thm (anim1d () ((anim1d.1 (-> ph (-> ps ch)))) (-> ph (-> (/\ ps th) (/\ ch th))) (anim1d.1 ph th idd anim12d)) thm (anim2d () ((anim1d.1 (-> ph (-> ps ch)))) (-> ph (-> (/\ th ps) (/\ th ch))) (ph th idd anim1d.1 anim12d)) thm (pm3.45 () () (-> (-> ph ps) (-> (/\ ph ch) (/\ ps ch))) ((-> ph ps) id ch anim1d)) thm (im2anan9 () ((im2an9.1 (-> ph (-> ps ch))) (im2an9.2 (-> th (-> ta et)))) (-> (/\ ph th) (-> (/\ ps ta) (/\ ch et))) (im2an9.1 th adantr im2an9.2 ph adantl anim12d)) thm (im2anan9r () ((im2an9.1 (-> ph (-> ps ch))) (im2an9.2 (-> th (-> ta et)))) (-> (/\ th ph) (-> (/\ ps ta) (/\ ch et))) (im2an9.1 th adantl im2an9.2 ph adantr anim12d)) thm (orim12d () ((orim12d.1 (-> ph (-> ps ch))) (orim12d.2 (-> ph (-> th ta)))) (-> ph (-> (\/ ps th) (\/ ch ta))) (ps ch th ta pm3.48 orim12d.1 orim12d.2 sylanc)) thm (orim1d () ((orim1d.1 (-> ph (-> ps ch)))) (-> ph (-> (\/ ps th) (\/ ch th))) (orim1d.1 ph th idd orim12d)) thm (orim2d () ((orim1d.1 (-> ph (-> ps ch)))) (-> ph (-> (\/ th ps) (\/ th ch))) (ph th idd orim1d.1 orim12d)) thm (orim2 () () (-> (-> ps ch) (-> (\/ ph ps) (\/ ph ch))) ((-> ps ch) id ph orim2d)) thm (pm2.73 () () (-> (-> ph ps) (-> (\/ (\/ ph ps) ch) (\/ ps ch))) (ph ps pm2.621 ch orim1d)) thm (pm2.74 () () (-> (-> ps ph) (-> (\/ (\/ ph ps) ch) (\/ ph ch))) (ps ph orel2 ch orim1d ph ch orc (\/ (\/ ph ps) ch) a1d ja)) thm (pm2.75 () () (-> (\/ ph ps) (-> (\/ ph (-> ps ch)) (\/ ph ch))) (ph ch orc (\/ ph (-> ps ch)) a1d ps ch pm2.27 ph orim2d jaoi)) thm (pm2.76 () () (-> (\/ ph (-> ps ch)) (-> (\/ ph ps) (\/ ph ch))) (ph ps ch pm2.75 com12)) thm (pm2.8 () () (-> (\/ ps ch) (-> (\/ (-. ch) th) (\/ ps th))) (ps th orc (\/ (-. ch) th) a1d ch ps pm2.24 th orim1d jaoi)) thm (pm2.81 () () (-> (-> ps (-> ch th)) (-> (\/ ph ps) (-> (\/ ph ch) (\/ ph th)))) (ps (-> ch th) ph orim2 ph ch th pm2.76 syl6)) thm (pm2.82 () () (-> (\/ (\/ ph ps) ch) (-> (\/ (\/ ph (-. ch)) th) (\/ (\/ ph ps) th))) ((\/ ph ps) (\/ ph (-. ch)) ax-1 ch ps pm2.24 ph orim2d jaoi th orim1d)) thm (pm2.85 () () (-> (-> (\/ ph ps) (\/ ph ch)) (\/ ph (-> ps ch))) ((\/ ph ps) (\/ ph ch) imor ph ps pm2.48 (\/ ph ch) orim1i sylbi ps ch imor ph orbi2i ph (-. ps) ch orordi bitr2 sylib)) thm (pm3.2ni () ((pm3.2ni.1 (-. ph)) (pm3.2ni.2 (-. ps))) (-. (\/ ph ps)) (pm3.2ni.1 pm3.2ni.2 pm3.2i ph ps ioran mpbir)) thm (orabs () () (<-> ph (/\ (\/ ph ps) ph)) (ph ps orc ancri (\/ ph ps) ph pm3.27 impbi)) thm (oranabs () () (<-> (/\ (\/ ph (-. ps)) ps) (/\ ph ps)) (ph ps pm3.2 ps (/\ ph ps) pm2.21 jaoi imp ph (-. ps) orc ps anim1i impbi)) thm (pm5.74 () () (<-> (-> ph (<-> ps ch)) (<-> (-> ph ps) (-> ph ch))) (ps ch bi1 ph imim2i a2d ps ch bi2 ph imim2i a2d impbid (-> ph ps) (-> ph ch) bi1 pm2.86d (-> ph ps) (-> ph ch) bi2 pm2.86d anim12d ph pm4.24 ps ch bi 3imtr4g impbi)) thm (pm5.74i () ((pm5.74i.1 (-> ph (<-> ps ch)))) (<-> (-> ph ps) (-> ph ch)) (pm5.74i.1 ph ps ch pm5.74 mpbi)) thm (pm5.74d () ((pm5.74d.1 (-> ph (-> ps (<-> ch th))))) (-> ph (<-> (-> ps ch) (-> ps th))) (pm5.74d.1 ps ch th pm5.74 sylib)) thm (pm5.74ri () ((pm5.74ri.1 (<-> (-> ph ps) (-> ph ch)))) (-> ph (<-> ps ch)) (pm5.74ri.1 ph ps ch pm5.74 mpbir)) thm (pm5.74rd () ((pm5.74rd.1 (-> ph (<-> (-> ps ch) (-> ps th))))) (-> ph (-> ps (<-> ch th))) (pm5.74rd.1 ps ch th pm5.74 sylibr)) thm (mpbidi () ((mpbidi.min (-> th (-> ph ps))) (mpbidi.maj (-> ph (<-> ps ch)))) (-> th (-> ph ch)) (mpbidi.min mpbidi.maj pm5.74i sylib)) thm (ibib () () (<-> (-> ph ps) (-> ph (<-> ph ps))) (ph ps pm3.4 ph ps pm3.26 ps a1d impbid exp ph ps bi1 com12 impbid pm5.74i)) thm (ibibr () () (<-> (-> ph ps) (-> ph (<-> ps ph))) (ph ps ibib ph ps bicom ph imbi2i bitr)) thm (ibi () ((ibi.1 (-> ph (<-> ph ps)))) (-> ph ps) (ibi.1 biimpd pm2.43i)) thm (ibir () ((ibir.1 (-> ph (<-> ps ph)))) (-> ph ps) (ibir.1 bicomd ibi)) thm (ibd () ((ibd.1 (-> ph (-> ps (<-> ps ch))))) (-> ph (-> ps ch)) (ibd.1 ps ch ibib sylibr)) thm (pm5.501 () () (-> ph (<-> ps (<-> ph ps))) (ph ps ibib pm5.74ri)) thm (ordi () () (<-> (\/ ph (/\ ps ch)) (/\ (\/ ph ps) (\/ ph ch))) (ps ch pm3.26 ph orim2i ps ch pm3.27 ph orim2i jca ph ps df-or (-. ph) ps ch pm3.43i ph ch df-or ph (/\ ps ch) df-or 3imtr4g sylbi imp impbi)) thm (ordir () () (<-> (\/ (/\ ph ps) ch) (/\ (\/ ph ch) (\/ ps ch))) (ch ph ps ordi (/\ ph ps) ch orcom ph ch orcom ps ch orcom anbi12i 3bitr4)) thm (jcab () () (<-> (-> ph (/\ ps ch)) (/\ (-> ph ps) (-> ph ch))) ((-. ph) ps ch ordi ph (/\ ps ch) imor ph ps imor ph ch imor anbi12i 3bitr4)) thm (pm4.76 () () (<-> (/\ (-> ph ps) (-> ph ch)) (-> ph (/\ ps ch))) (ph ps ch jcab bicomi)) thm (jcad () ((jcad.1 (-> ph (-> ps ch))) (jcad.2 (-> ph (-> ps th)))) (-> ph (-> ps (/\ ch th))) (jcad.1 imp jcad.2 imp jca exp)) thm (jctild () ((jctild.1 (-> ph (-> ps ch))) (jctild.2 (-> ph th))) (-> ph (-> ps (/\ th ch))) (jctild.2 ps a1d jctild.1 jcad)) thm (jctird () ((jctird.1 (-> ph (-> ps ch))) (jctird.2 (-> ph th))) (-> ph (-> ps (/\ ch th))) (jctird.1 jctird.2 ps a1d jcad)) thm (pm3.43 () () (-> (/\ (-> ph ps) (-> ph ch)) (-> ph (/\ ps ch))) (ph ps ch jcab biimpr)) thm (andi () () (<-> (/\ ph (\/ ps ch)) (\/ (/\ ph ps) (/\ ph ch))) ((-. ph) (-. ps) (-. ch) ordi ps ch ioran (-. ph) orbi2i ph ps ianor ph ch ianor anbi12i 3bitr4 negbii ph (\/ ps ch) anor (/\ ph ps) (/\ ph ch) oran 3bitr4)) thm (andir () () (<-> (/\ (\/ ph ps) ch) (\/ (/\ ph ch) (/\ ps ch))) (ch ph ps andi (\/ ph ps) ch ancom ph ch ancom ps ch ancom orbi12i 3bitr4)) thm (orddi () () (<-> (\/ (/\ ph ps) (/\ ch th)) (/\ (/\ (\/ ph ch) (\/ ph th)) (/\ (\/ ps ch) (\/ ps th)))) (ph ps (/\ ch th) ordir ph ch th ordi ps ch th ordi anbi12i bitr)) thm (anddi () () (<-> (/\ (\/ ph ps) (\/ ch th)) (\/ (\/ (/\ ph ch) (/\ ph th)) (\/ (/\ ps ch) (/\ ps th)))) (ph ps (\/ ch th) andir ph ch th andi ps ch th andi orbi12i bitr)) thm (bibi2i () ((bibi.a (<-> ph ps))) (<-> (<-> ch ph) (<-> ch ps)) (ch ph bi bibi.a ch imbi1i (-> ch ph) anbi2i bibi.a ch imbi2i (-> ps ch) anbi1i ch ps bi bitr4 3bitr)) thm (bibi1i () ((bibi.a (<-> ph ps))) (<-> (<-> ph ch) (<-> ps ch)) (ph ch bicom bibi.a ch bibi2i ch ps bicom 3bitr)) thm (bibi12i () ((bibi.a (<-> ph ps)) (bibi12.2 (<-> ch th))) (<-> (<-> ph ch) (<-> ps th)) (bibi12.2 ph bibi2i bibi.a th bibi1i bitr)) thm (negbid () ((bid.1 (-> ph (<-> ps ch)))) (-> ph (<-> (-. ps) (-. ch))) (bid.1 ps ch pm4.11 sylib)) thm (imbi2d () ((bid.1 (-> ph (<-> ps ch)))) (-> ph (<-> (-> th ps) (-> th ch))) (bid.1 th a1d pm5.74d)) thm (imbi1d () ((bid.1 (-> ph (<-> ps ch)))) (-> ph (<-> (-> ps th) (-> ch th))) (bid.1 negbid (-. th) imbi2d ps th pm4.1 ch th pm4.1 3bitr4g)) thm (orbi2d () ((bid.1 (-> ph (<-> ps ch)))) (-> ph (<-> (\/ th ps) (\/ th ch))) (bid.1 (-. th) imbi2d th ps df-or th ch df-or 3bitr4g)) thm (orbi1d () ((bid.1 (-> ph (<-> ps ch)))) (-> ph (<-> (\/ ps th) (\/ ch th))) (bid.1 th orbi2d ps th orcom ch th orcom 3bitr4g)) thm (anbi2d () ((bid.1 (-> ph (<-> ps ch)))) (-> ph (<-> (/\ th ps) (/\ th ch))) (bid.1 biimpd th anim2d bid.1 biimprd th anim2d impbid)) thm (anbi1d () ((bid.1 (-> ph (<-> ps ch)))) (-> ph (<-> (/\ ps th) (/\ ch th))) (bid.1 th anbi2d ps th ancom ch th ancom 3bitr4g)) thm (bibi2d () ((bid.1 (-> ph (<-> ps ch)))) (-> ph (<-> (<-> th ps) (<-> th ch))) (bid.1 th imbi2d (-> ps th) anbi1d bid.1 th imbi1d (-> th ch) anbi2d bitrd th ps bi th ch bi 3bitr4g)) thm (bibi1d () ((bid.1 (-> ph (<-> ps ch)))) (-> ph (<-> (<-> ps th) (<-> ch th))) (bid.1 th bibi2d ps th bicom ch th bicom 3bitr4g)) thm (orbi1 () () (-> (<-> ph ps) (<-> (\/ ph ch) (\/ ps ch))) ((<-> ph ps) id ch orbi1d)) thm (anbi1 () () (-> (<-> ph ps) (<-> (/\ ph ch) (/\ ps ch))) ((<-> ph ps) id ch anbi1d)) thm (pm4.22 () () (-> (/\ (<-> ph ps) (<-> ps ch)) (<-> ph ch)) ((<-> ph ps) id ch bibi1d biimpar)) thm (imbi1 () () (-> (<-> ph ps) (<-> (-> ph ch) (-> ps ch))) ((<-> ph ps) id ch imbi1d)) thm (imbi2 () () (-> (<-> ph ps) (<-> (-> ch ph) (-> ch ps))) ((<-> ph ps) ch ax-1 pm5.74d)) thm (bibi1 () () (-> (<-> ph ps) (<-> (<-> ph ch) (<-> ps ch))) ((<-> ph ps) id ch bibi1d)) thm (imbi12d () ((bi12d.1 (-> ph (<-> ps ch))) (bi12d.2 (-> ph (<-> th ta)))) (-> ph (<-> (-> ps th) (-> ch ta))) (bi12d.1 th imbi1d bi12d.2 ch imbi2d bitrd)) thm (orbi12d () ((bi12d.1 (-> ph (<-> ps ch))) (bi12d.2 (-> ph (<-> th ta)))) (-> ph (<-> (\/ ps th) (\/ ch ta))) (bi12d.1 th orbi1d bi12d.2 ch orbi2d bitrd)) thm (anbi12d () ((bi12d.1 (-> ph (<-> ps ch))) (bi12d.2 (-> ph (<-> th ta)))) (-> ph (<-> (/\ ps th) (/\ ch ta))) (bi12d.1 th anbi1d bi12d.2 ch anbi2d bitrd)) thm (bibi12d () ((bi12d.1 (-> ph (<-> ps ch))) (bi12d.2 (-> ph (<-> th ta)))) (-> ph (<-> (<-> ps th) (<-> ch ta))) (bi12d.1 th bibi1d bi12d.2 ch bibi2d bitrd)) thm (pm4.39 () () (-> (/\ (<-> ph ch) (<-> ps th)) (<-> (\/ ph ps) (\/ ch th))) ((<-> ph ch) (<-> ps th) pm3.26 (<-> ph ch) (<-> ps th) pm3.27 orbi12d)) thm (pm4.38 () () (-> (/\ (<-> ph ch) (<-> ps th)) (<-> (/\ ph ps) (/\ ch th))) ((<-> ph ch) (<-> ps th) pm3.26 (<-> ph ch) (<-> ps th) pm3.27 anbi12d)) thm (bi2anan9 () ((bi2an9.1 (-> ph (<-> ps ch))) (bi2an9.2 (-> th (<-> ta et)))) (-> (/\ ph th) (<-> (/\ ps ta) (/\ ch et))) (bi2an9.1 ta anbi1d bi2an9.2 ch anbi2d sylan9bb)) thm (bi2anan9r () ((bi2an9.1 (-> ph (<-> ps ch))) (bi2an9.2 (-> th (<-> ta et)))) (-> (/\ th ph) (<-> (/\ ps ta) (/\ ch et))) (bi2an9.1 bi2an9.2 bi2anan9 ancoms)) thm (bi2bian9 () ((bi2an9.1 (-> ph (<-> ps ch))) (bi2an9.2 (-> th (<-> ta et)))) (-> (/\ ph th) (<-> (<-> ps ta) (<-> ch et))) (bi2an9.1 th adantr bi2an9.2 ph adantl bibi12d)) thm (pm4.71 () () (<-> (-> ph ps) (<-> ph (/\ ph ps))) (ph ps ancl ph ps pm3.26 (-> ph ps) a1i impbid ph (/\ ph ps) bi1 ph ps pm3.27 syl6 impbi)) thm (pm4.71r () () (<-> (-> ph ps) (<-> ph (/\ ps ph))) (ph ps pm4.71 ph ps ancom ph bibi2i bitr)) thm (pm4.71i () ((pm4.71i.1 (-> ph ps))) (<-> ph (/\ ph ps)) (pm4.71i.1 ph ps pm4.71 mpbi)) thm (pm4.71ri () ((pm4.71ri.1 (-> ph ps))) (<-> ph (/\ ps ph)) (pm4.71ri.1 ph ps pm4.71r mpbi)) thm (pm4.71rd () ((pm4.71rd.1 (-> ph (-> ps ch)))) (-> ph (<-> ps (/\ ch ps))) (pm4.71rd.1 ps ch pm4.71r sylib)) thm (pm4.45 () () (<-> ph (/\ ph (\/ ph ps))) (ph ps orc pm4.71i)) thm (pm4.72 () () (<-> (-> ph ps) (<-> ps (\/ ph ps))) (ps ph olc (-> ph ps) a1i ph ps pm2.621 impbid ps (\/ ph ps) bi2 ph ps pm2.67 syl impbi)) thm (iba () () (-> ph (<-> ps (/\ ps ph))) (ph ps ancrb pm5.74ri)) thm (ibar () () (-> ph (<-> ps (/\ ph ps))) (ph ps anclb pm5.74ri)) thm (pm5.32 () () (<-> (-> ph (<-> ps ch)) (<-> (/\ ph ps) (/\ ph ch))) (ps ch pm4.11 ph imbi2i ph (-. ps) (-. ch) pm5.74 (-> ph (-. ps)) (-> ph (-. ch)) pm4.11 3bitr ph ps df-an ph ch df-an bibi12i bitr4)) thm (pm5.32i () ((pm5.32i.1 (-> ph (<-> ps ch)))) (<-> (/\ ph ps) (/\ ph ch)) (pm5.32i.1 ph ps ch pm5.32 mpbi)) thm (pm5.32ri () ((pm5.32i.1 (-> ph (<-> ps ch)))) (<-> (/\ ps ph) (/\ ch ph)) (pm5.32i.1 pm5.32i ps ph ancom ch ph ancom 3bitr4)) thm (pm5.32d () ((pm5.32d.1 (-> ph (-> ps (<-> ch th))))) (-> ph (<-> (/\ ps ch) (/\ ps th))) (pm5.32d.1 ps ch th pm5.32 sylib)) thm (pm5.32rd () ((pm5.32d.1 (-> ph (-> ps (<-> ch th))))) (-> ph (<-> (/\ ch ps) (/\ th ps))) (pm5.32d.1 pm5.32d ch ps ancom th ps ancom 3bitr4g)) thm (pm5.33 () () (<-> (/\ ph (-> ps ch)) (/\ ph (-> (/\ ph ps) ch))) (ph ps ibar ch imbi1d pm5.32i)) thm (pm5.36 () () (<-> (/\ ph (<-> ph ps)) (/\ ps (<-> ph ps))) ((<-> ph ps) id pm5.32ri)) thm (pm5.42 () () (<-> (-> ph (-> ps ch)) (-> ph (-> ps (/\ ph ch)))) (ph ch ibar ps imbi2d pm5.74i)) thm (oibabs () () (<-> (<-> ph ps) (-> (\/ ph ps) (<-> ph ps))) ((<-> ph ps) (\/ ph ps) ax-1 ph ps orc (<-> ph ps) imim1i ibd ps ph olc (<-> ph ps) imim1i ps ph ibib ps ph bicom ps imbi2i bitr sylibr impbid impbi)) thm (exmid () () (\/ ph (-. ph)) ((-. ph) id orri)) thm (pm2.1 () () (\/ (-. ph) ph) (ph nega orri)) thm (pm2.13 () () (\/ ph (-. (-. (-. ph)))) ((-. ph) negb orri)) thm (pm3.24 () () (-. (/\ ph (-. ph))) ((-. ph) exmid ph (-. ph) ianor mpbir)) thm (pm2.26 () () (\/ (-. ph) (-> (-> ph ps) ps)) (ph nega ps imim1i com12 orri)) thm (pm5.18 () () (<-> (<-> ph ps) (-. (<-> ph (-. ps)))) (ph ps bicom ph (-. ps) bicom ps ph pm2.61 ps ph pm2.65 ph ps con2 syl5 anim12d (-. ps) ph bi syl5ib ph ps annim syl6ib com12 (-> ps ph) (-> ph ps) imnan sylib ps ph bi negbii sylibr ps ph bi negbii ps ph pm2.5 ps ph annim ph (-. ps) pm2.21 ps adantl sylbir jca ph ps annim ph (-. ps) ax-1 (-. ps) adantr sylbir ph ps pm2.51 jca jaoi (-> ps ph) (-> ph ps) ianor (-. ps) ph bi 3imtr4 sylbi impbi bitr bicon2i bitr)) thm (nbbn () () (<-> (<-> (-. ph) ps) (-. (<-> ph ps))) ((-. ph) ps bicom ph ps bicom ps ph pm5.18 bitr bicon2i bitr)) thm (pm5.11 () () (\/ (-> ph ps) (-> (-. ph) ps)) (ph ps pm2.5 orri)) thm (pm5.12 () () (\/ (-> ph ps) (-> ph (-. ps))) (ph ps pm2.51 orri)) thm (pm5.13 () () (\/ (-> ph ps) (-> ps ph)) (ph ps pm2.521 orri)) thm (pm5.14 () () (\/ (-> ph ps) (-> ps ch)) (ps ph ax-1 con3i ch pm2.21d orri)) thm (pm5.15 () () (\/ (<-> ph ps) (<-> ph (-. ps))) (ph ps pm5.18 biimpr con1i orri)) thm (pm5.16 () () (-. (/\ (<-> ph ps) (<-> ph (-. ps)))) (ph ps pm5.18 biimp (<-> ph ps) (<-> ph (-. ps)) pm4.62 mpbi (<-> ph ps) (<-> ph (-. ps)) ianor mpbir)) thm (pm5.17 () () (<-> (/\ (\/ ph ps) (-. (/\ ph ps))) (<-> ph (-. ps))) (ph ps orcom ps ph df-or bitr ph ps imnan bicomi anbi12i (-. ps) ph bi bitr4 (-. ps) ph bicom bitr)) thm (pm5.19 () () (-. (<-> ph (-. ph))) (ph pm4.2 ph ph pm5.18 mpbi)) thm (dfbi () () (<-> (<-> ph ps) (\/ (/\ ph ps) (/\ (-. ph) (-. ps)))) (ph ps pm5.18 ph ps imnan ps ph bi2.15 (-. ph) ps iman bitr anbi12i ph (-. ps) bi (/\ ph ps) (/\ (-. ph) (-. ps)) ioran 3bitr4r bicon1i bitr)) thm (xor () () (<-> (-. (<-> ph ps)) (\/ (/\ ph (-. ps)) (/\ ps (-. ph)))) ((-. ph) ps dfbi ph ps nbbn ps (-. ph) ancom ph pm4.13 (-. ps) anbi1i orbi12i (/\ ps (-. ph)) (/\ ph (-. ps)) orcom bitr3 3bitr3)) thm (pm5.24 () () (<-> (-. (\/ (/\ ph ps) (/\ (-. ph) (-. ps)))) (\/ (/\ ph (-. ps)) (/\ ps (-. ph)))) (ph ps dfbi negbii ph ps xor bitr3)) thm (xor2 () () (<-> (-. (<-> ph ps)) (/\ (\/ ph ps) (-. (/\ ph ps)))) (ph ps xor (/\ ph ps) (/\ (-. ph) (-. ps)) ioran ph ps pm5.24 ph ps oran (-. (/\ ph ps)) anbi2i (-. (/\ ph ps)) (\/ ph ps) ancom bitr3 3bitr3 bitr)) thm (pm5.55 () () (\/ (<-> (\/ ph ps) ph) (<-> (\/ ph ps) ps)) (ps ph pm5.13 ps ph pm4.72 ps ph orcom ph bibi2i ph (\/ ph ps) bicom 3bitr ph ps pm4.72 ps (\/ ph ps) bicom bitr orbi12i mpbi)) thm (pm5.1 () () (-> (/\ ph ps) (<-> ph ps)) (ph ps pm5.501 biimpa)) thm (pm5.21 () () (-> (/\ (-. ph) (-. ps)) (<-> ph ps)) ((-. ph) (-. ps) pm5.1 bicon4d)) thm (pm5.21ni () ((pm5.21ni.1 (-> ph ps)) (pm5.21ni.2 (-> ch ps))) (-> (-. ps) (<-> ph ch)) (ph ch pm5.21 pm5.21ni.1 con3i pm5.21ni.2 con3i sylanc)) thm (pm5.21nii () ((pm5.21ni.1 (-> ph ps)) (pm5.21ni.2 (-> ch ps)) (pm5.21nii.3 (-> ps (<-> ph ch)))) (<-> ph ch) (pm5.21nii.3 pm5.21ni.1 pm5.21ni.2 pm5.21ni pm2.61i)) thm (pm5.35 () () (-> (/\ (-> ph ps) (-> ph ch)) (-> ph (<-> ps ch))) ((-> ph ps) (-> ph ch) pm5.1 pm5.74rd)) thm (pm5.54 () () (\/ (<-> (/\ ph ps) ph) (<-> (/\ ph ps) ps)) ((/\ ph ps) ph pm5.1 anabss1 ps ph iba bicomd pm5.21ni orri)) thm (elimant () () (-> (/\ (-> ph ps) (-> (-> ps ch) (-> ph th))) (-> ph (-> ch th))) ((-> ph ps) id impac ps ph pm5.1 syl ch imbi1d (-> ph th) imbi1d biimpd exp com23 imp ph ch th imdi syl6ibr pm2.43d)) thm (baib () ((baib.1 (<-> ph (/\ ps ch)))) (-> ps (<-> ph ch)) (ps ch ibar baib.1 syl6rbbr)) thm (baibr () ((baibr.1 (<-> ph (/\ ps ch)))) (-> ps (<-> ch ph)) (baibr.1 baib bicomd)) thm (pm5.44 () () (-> (-> ph ps) (<-> (-> ph ch) (-> ph (/\ ps ch)))) (ph ps ch jcab baibr)) thm (msca () ((msca.1 (-> ph (-> ps ch))) (msca.2 (-> th (-> ps (-. ch))))) (-> ph (-> ps (-. th))) (ph ps pm3.27 msca.1 imp jc msca.2 nsyl exp)) thm (orcana () () (<-> (-> ph (\/ ps ch)) (-> (/\ ph (-. ps)) ch)) (ps ch df-or ph imbi2i ph (-. ps) ch impexp bitr4)) thm (pm5.6 () () (<-> (-> (/\ ph (-. ps)) ch) (-> ph (\/ ps ch))) (ph ps ch orcana bicomi)) thm (orbidi () () (<-> (\/ ph (<-> ps ch)) (<-> (\/ ph ps) (\/ ph ch))) (ph ch orc (\/ ph ps) a1d ph ps orc (\/ ph ch) a1d impbid (<-> ps ch) id ph orbi2d jaoi ph ps ch pm2.85 ph ch ps pm2.85 anim12i (\/ ph ps) (\/ ph ch) bi ps ch bi ph orbi2i ph (-> ps ch) (-> ch ps) ordi bitr 3imtr4 impbi)) thm (biass () () (<-> (<-> (<-> ph ps) ch) (<-> ph (<-> ps ch))) (ph (/\ ps ch) (/\ (-. ps) (-. ch)) andi ps ch dfbi ph anbi2i ph ps ch anass ph (-. ps) (-. ch) anass orbi12i 3bitr4 (-. ph) (/\ ps (-. ch)) (/\ (-. ps) ch) andi ps ch xor ch (-. ps) ancom (/\ ps (-. ch)) orbi2i bitr (-. ph) anbi2i (-. ph) ps (-. ch) anass (-. ph) (-. ps) ch anass orbi12i 3bitr4 orbi12i ph (<-> ps ch) dfbi (<-> ph ps) ch dfbi ph ps dfbi ch anbi1i (/\ ph ps) (/\ (-. ph) (-. ps)) ch andir bitr ph ps xor ps (-. ph) ancom (/\ ph (-. ps)) orbi2i bitr (-. ch) anbi1i (/\ ph (-. ps)) (/\ (-. ph) ps) (-. ch) andir bitr orbi12i (/\ (/\ ph ps) ch) (/\ (/\ (-. ph) (-. ps)) ch) (/\ (/\ ph (-. ps)) (-. ch)) (/\ (/\ (-. ph) ps) (-. ch)) or42 3bitr 3bitr4r)) thm (biluk () () (<-> (<-> ph ps) (<-> (<-> ch ps) (<-> ph ch))) (ph ps bicom ch bibi1i ps ph ch biass bitr (<-> ph ps) ch (<-> ps (<-> ph ch)) biass mpbi ch ps (<-> ph ch) biass bitr4)) thm (pm5.7 () () (<-> (<-> (\/ ph ch) (\/ ps ch)) (\/ ch (<-> ph ps))) (ch ph ps orbidi ch ph orcom ch ps orcom bibi12i bitr2)) thm (bigolden () () (<-> (<-> (/\ ph ps) ph) (<-> ps (\/ ph ps))) (ph ps pm4.71 ph ps pm4.72 ph (/\ ph ps) bicom 3bitr3r)) thm (pm5.71 () () (-> (-> ps (-. ch)) (<-> (/\ (\/ ph ps) ch) (/\ ph ch))) (ps ph orel2 ph ps orc (-. ps) a1i impbid ch anbi1d ch (<-> (\/ ph ps) ph) pm2.21 pm5.32rd ja)) thm (pm5.75 () () (-> (/\ (-> ch (-. ps)) (<-> ph (\/ ps ch))) (<-> (/\ ph (-. ps)) ch)) (ph (\/ ps ch) bi1 ph ps ch pm5.6 sylibr (-> ch (-. ps)) adantl ph (\/ ps ch) bi2 ch ps olc ph ps olc imim12i syl ch ps ph pm5.6 sylibr exp3a a2d impcom (-> ch (-. ps)) (<-> ph (\/ ps ch)) pm3.26 jcad impbid)) thm (nan () () (<-> (-> ph (-. (/\ ps ch))) (-> (/\ ph ps) (-. ch))) (ph ps (-. ch) impexp ps ch imnan ph imbi2i bitr2)) thm (orcanai () ((orcanai.1 (-> ph (\/ ps ch)))) (-> (/\ ph (-. ps)) ch) (orcanai.1 ord imp)) thm (intnan () ((intnan.1 (-. ph))) (-. (/\ ps ph)) (intnan.1 ps ph pm3.27 mto)) thm (intnanr () ((intnan.1 (-. ph))) (-. (/\ ph ps)) (intnan.1 ph ps pm3.26 mto)) thm (intnand () ((intnand.1 (-> ph (-. ps)))) (-> ph (-. (/\ ch ps))) (intnand.1 ch ps pm3.27 nsyl)) thm (intnanrd () ((intnand.1 (-> ph (-. ps)))) (-> ph (-. (/\ ps ch))) (intnand.1 ps ch pm3.26 nsyl)) thm (mpan () ((mpan.1 ph) (mpan.2 (-> (/\ ph ps) ch))) (-> ps ch) (mpan.1 mpan.2 exp ax-mp)) thm (mpan2 () ((mpan2.1 ps) (mpan2.2 (-> (/\ ph ps) ch))) (-> ph ch) (mpan2.1 mpan2.2 exp mpi)) thm (mp2an () ((mp2an.1 ph) (mp2an.2 ps) (mp2an.3 (-> (/\ ph ps) ch))) ch (mp2an.2 mp2an.1 mp2an.3 mpan ax-mp)) thm (mpani () ((mpani.1 ps) (mpani.2 (-> ph (-> (/\ ps ch) th)))) (-> ph (-> ch th)) (mpani.1 mpani.2 exp3a mpi)) thm (mpan2i () ((mpan2i.1 ch) (mpan2i.2 (-> ph (-> (/\ ps ch) th)))) (-> ph (-> ps th)) (mpan2i.1 mpan2i.2 exp3a mpii)) thm (mp2ani () ((mp2ani.1 ps) (mp2ani.2 ch) (mp2ani.3 (-> ph (-> (/\ ps ch) th)))) (-> ph th) (mp2ani.2 mp2ani.1 mp2ani.3 mpani mpi)) thm (mpand () ((mpand.1 (-> ph ps)) (mpand.2 (-> ph (-> (/\ ps ch) th)))) (-> ph (-> ch th)) (mpand.1 mpand.2 exp3a mpd)) thm (mpan2d () ((mpan2d.1 (-> ph ch)) (mpan2d.2 (-> ph (-> (/\ ps ch) th)))) (-> ph (-> ps th)) (mpan2d.1 mpan2d.2 exp3a mpid)) thm (mp2and () ((mp2and.1 (-> ph ps)) (mp2and.2 (-> ph ch)) (mp2and.3 (-> ph (-> (/\ ps ch) th)))) (-> ph th) (mp2and.2 mp2and.1 mp2and.3 mpand mpd)) thm (mpdan () ((mpdan.1 (-> ph ps)) (mpdan.2 (-> (/\ ph ps) ch))) (-> ph ch) (mpdan.1 mpdan.2 exp mpd)) thm (mpancom () ((mpancom.1 (-> ps ph)) (mpancom.2 (-> (/\ ph ps) ch))) (-> ps ch) (mpancom.1 mpancom.2 ancoms mpdan)) thm (mpanl1 () ((mpanl1.1 ph) (mpanl1.2 (-> (/\ (/\ ph ps) ch) th))) (-> (/\ ps ch) th) (mpanl1.1 mpanl1.2 exp mpan imp)) thm (mpanl2 () ((mpanl2.1 ps) (mpanl2.2 (-> (/\ (/\ ph ps) ch) th))) (-> (/\ ph ch) th) (mpanl2.1 mpanl2.2 exp mpan2 imp)) thm (mpanl12 () ((mpanl12.1 ph) (mpanl12.2 ps) (mpanl12.3 (-> (/\ (/\ ph ps) ch) th))) (-> ch th) (mpanl12.2 mpanl12.1 mpanl12.3 mpanl1 mpan)) thm (mpanr1 () ((mpanr1.1 ps) (mpanr1.2 (-> (/\ ph (/\ ps ch)) th))) (-> (/\ ph ch) th) (mpanr1.1 mpanr1.2 exp mpani imp)) thm (mpanr2 () ((mpanr2.1 ch) (mpanr2.2 (-> (/\ ph (/\ ps ch)) th))) (-> (/\ ph ps) th) (mpanr2.1 mpanr2.2 exp mpan2i imp)) thm (mpanlr1 () ((mpanlr1.1 ps) (mpanlr1.2 (-> (/\ (/\ ph (/\ ps ch)) th) ta))) (-> (/\ (/\ ph ch) th) ta) (mpanlr1.1 mpanlr1.2 exp mpanr1 imp)) thm (mtt () () (-> (-. ph) (<-> (-. ps) (-> ps ph))) (ps ph pm2.21 (-. ph) a1i ps ph con3 com12 impbid)) thm (mt2bi () ((mt2bi.1 ph)) (<-> (-. ps) (-> ps (-. ph))) (ps (-. ph) pm2.21 mt2bi.1 ps ph con2 mpi impbi)) thm (mtbid () ((mtbid.min (-> ph (-. ps))) (mtbid.maj (-> ph (<-> ps ch)))) (-> ph (-. ch)) (mtbid.min mtbid.maj biimprd mtod)) thm (mtbird () ((mtbird.min (-> ph (-. ch))) (mtbird.maj (-> ph (<-> ps ch)))) (-> ph (-. ps)) (mtbird.min mtbird.maj biimpd mtod)) thm (mtbii () ((mtbii.min (-. ps)) (mtbii.maj (-> ph (<-> ps ch)))) (-> ph (-. ch)) (mtbii.min mtbii.maj biimprd mtoi)) thm (mtbiri () ((mtbiri.min (-. ch)) (mtbiri.maj (-> ph (<-> ps ch)))) (-> ph (-. ps)) (mtbiri.min mtbiri.maj biimpd mtoi)) thm (2th () ((2th.1 ph) (2th.2 ps)) (<-> ph ps) (2th.2 ph a1i 2th.1 ps a1i impbi)) thm (2false () ((2false.1 (-. ph)) (2false.2 (-. ps))) (<-> ph ps) (2false.1 2false.2 ph ps pm5.21 mp2an)) thm (tbt () ((tbt.1 ph)) (<-> ps (<-> ps ph)) (tbt.1 ps a1i ps a1d ps ph ax-1 impbid tbt.1 ps ph bi2 mpi impbi)) thm (nbn () ((nbn.1 (-. ph))) (<-> (-. ps) (<-> ps ph)) (ps ph pm2.21 nbn.1 (-. ps) a1i ps pm2.21d impbid nbn.1 ps ph bi1 mtoi impbi)) thm (biantru () ((biantru.1 ph)) (<-> ps (/\ ps ph)) (biantru.1 ph ps iba ax-mp)) thm (biantrur () ((biantrur.1 ph)) (<-> ps (/\ ph ps)) (biantrur.1 ph ps ibar ax-mp)) thm (biantrud () ((biantrud.1 (-> ph ps))) (-> ph (<-> ch (/\ ch ps))) (biantrud.1 ch anim2i expcom ch ps pm3.26 ph a1i impbid)) thm (biantrurd () ((biantrud.1 (-> ph ps))) (-> ph (<-> ch (/\ ps ch))) (biantrud.1 ch biantrud ch ps ancom syl6bb)) thm (mpbiran () ((mpbiran.1 (<-> ph (/\ ps ch))) (mpbiran.2 ps)) (<-> ph ch) (mpbiran.1 mpbiran.2 ch biantrur bitr4)) thm (mpbiran2 () ((mpbiran.1 (<-> ph (/\ ps ch))) (mpbiran2.2 ch)) (<-> ph ps) (mpbiran.1 mpbiran2.2 ps biantru bitr4)) thm (mpbir2an () ((mpbiran.1 (<-> ph (/\ ps ch))) (mpbir2an.2 ps) (mpbir2an.3 ch)) ph (mpbir2an.3 mpbiran.1 mpbir2an.2 mpbiran mpbir)) thm (biimt () () (-> ph (<-> ps (-> ph ps))) (ps ph ax-1 ph a1i ph ps pm2.27 impbid)) thm (pm5.5 () () (-> ph (<-> (-> ph ps) ps)) (ph ps biimt bicomd)) thm (pm5.62 () () (<-> (\/ (/\ ph ps) (-. ps)) (\/ ph (-. ps))) (ph ps (-. ps) ordir ps exmid mpbiran2)) thm (biort () () (-> ph (<-> ph (\/ ph ps))) (ph ps orc ph a1d ph (\/ ph ps) ax-1 impbid)) thm (biorf () () (-> (-. ph) (<-> ps (\/ ph ps))) ((-. ph) ps biimt ph ps df-or syl6bbr)) thm (biorfi () ((biorfi.1 (-. ph))) (<-> ps (\/ ps ph)) (biorfi.1 ph ps biorf ax-mp ph ps orcom bitr)) thm (bianfi () ((bianfi.1 (-. ph))) (<-> ph (/\ ps ph)) (bianfi.1 (/\ ps ph) pm2.21i ps ph pm3.27 impbi)) thm (bianfd () ((bianfd.1 (-> ph (-. ps)))) (-> ph (<-> ps (/\ ps ch))) (bianfd.1 (/\ ps ch) pm2.21d ps ch pm3.26 ph a1i impbid)) thm (pm4.82 () () (<-> (/\ (-> ph ps) (-> ph (-. ps))) (-. ph)) (ph ps pm2.65 imp ph ps pm2.21 ph (-. ps) pm2.21 jca impbi)) thm (pm4.83 () () (<-> (/\ (-> ph ps) (-> (-. ph) ps)) ps) (ph exmid ps a1bi ph (-. ph) ps jaob bitr2)) thm (pclem6 () () (-> (<-> ph (/\ ps (-. ph))) (-. ps)) (ph (/\ ps (-. ph)) bi1 ps (-. ph) pm3.27 syl6 pm2.01d ph (/\ ps (-. ph)) bi2 exp3a com23 ps ph con3 syli mpd)) thm (biantr () () (-> (/\ (<-> ph ps) (<-> ch ps)) (<-> ph ch)) ((<-> ch ps) id ph bibi2d biimparc)) thm (bimsc1 () () (-> (/\ (-> ph ps) (<-> ch (/\ ps ph))) (<-> ch ph)) ((<-> ch (/\ ps ph)) id ph ps pm4.71r biimp bicomd sylan9bbr)) thm (ecase2d () ((ecase2d.1 (-> ph ps)) (ecase2d.2 (-> ph (-. (/\ ps ch)))) (ecase2d.3 (-> ph (-. (/\ ps th)))) (ecase2d.4 (-> ph (\/ ta (\/ ch th))))) (-> ph ta) (ecase2d.1 ecase2d.2 ps ch imnan sylibr mpd ecase2d.1 ecase2d.3 ps th imnan sylibr mpd jca ch th ioran sylibr ecase2d.4 ta (\/ ch th) orcom sylib ord mpd)) thm (ecase3 () ((ecase3.1 (-> ph ch)) (ecase3.2 (-> ps ch)) (ecase3.3 (-> (-. (\/ ph ps)) ch))) ch (ph ps ioran ecase3.3 sylbir exp ecase3.1 ecase3.2 pm2.61ii)) thm (ecase () ((ecase.1 (-> (-. ph) ch)) (ecase.2 (-> (-. ps) ch)) (ecase.3 (-> (/\ ph ps) ch))) ch (ecase.3 exp ecase.1 ecase.2 pm2.61nii)) thm (ecase3d () ((ecase3d.1 (-> ph (-> ps th))) (ecase3d.2 (-> ph (-> ch th))) (ecase3d.3 (-> ph (-> (-. (\/ ps ch)) th)))) (-> ph th) (ecase3d.1 com12 ecase3d.2 com12 ecase3d.3 com12 ecase3)) thm (caselem () () (<-> (/\ (\/ ph ps) (\/ ch th)) (\/ (\/ (/\ ph ch) (/\ ps ch)) (\/ (/\ ph th) (/\ ps th)))) ((\/ ph ps) ch th andi ph ps ch andir ph ps th andir orbi12i bitr)) thm (ccase () ((ccase.1 (-> (/\ ph ps) ta)) (ccase.2 (-> (/\ ch ps) ta)) (ccase.3 (-> (/\ ph th) ta)) (ccase.4 (-> (/\ ch th) ta))) (-> (/\ (\/ ph ch) (\/ ps th)) ta) (ph ch ps th caselem ccase.1 ccase.2 jaoi ccase.3 ccase.4 jaoi jaoi sylbi)) thm (ccased () ((ccased.1 (-> ph (-> (/\ ps ch) et))) (ccased.2 (-> ph (-> (/\ th ch) et))) (ccased.3 (-> ph (-> (/\ ps ta) et))) (ccased.4 (-> ph (-> (/\ th ta) et)))) (-> ph (-> (/\ (\/ ps th) (\/ ch ta)) et)) (ccased.1 ccased.2 jaod ccased.3 ccased.4 jaod jaod ps th ch ta caselem syl5ib)) thm (ccase2 () ((ccase2.1 (-> (/\ ph ps) ta)) (ccase2.2 (-> ch ta)) (ccase2.3 (-> th ta))) (-> (/\ (\/ ph ch) (\/ ps th)) ta) (ccase2.1 ccase2.2 ps adantr ccase2.3 ph adantl ccase2.3 ch adantl ccase)) thm (4cases () ((4cases.1 (-> (/\ ph ps) ch)) (4cases.2 (-> (/\ ph (-. ps)) ch)) (4cases.3 (-> (/\ (-. ph) ps) ch)) (4cases.4 (-> (/\ (-. ph) (-. ps)) ch))) ch (4cases.1 4cases.3 pm2.61an1 4cases.2 4cases.4 pm2.61an1 pm2.61i)) thm (niabn () ((niabn.1 ph)) (-> (-. ps) (<-> (/\ ch ps) (-. ph))) (ch ps pm3.27 niabn.1 ps pm2.21ni pm5.21ni)) thm (dedlem0a () () (-> ph (<-> ps (-> (-> ch ph) (/\ ps ph)))) (ps (-> ch ph) ax-1 ph a1i ph ch ax-1 ps imim1i com12 impbid ph ps iba (-> ch ph) imbi2d bitrd)) thm (dedlem0b () () (-> (-. ph) (<-> ps (-> (-> ps ph) (/\ ch ph)))) (ph (/\ ch ph) pm2.21 ps imim2d com23 ps ph pm2.21 ch ph pm3.27 imim12i con1d com12 impbid)) thm (dedlema () () (-> ph (<-> ps (\/ (/\ ps ph) (/\ ch (-. ph))))) (ps (/\ ch (-. ph)) orc ph a1i ph ps idd ph ps pm2.24 ch adantld jaod impbid ph ps iba (/\ ch (-. ph)) orbi1d bitrd)) thm (dedlemb () () (-> (-. ph) (<-> ch (\/ (/\ ps ph) (/\ ch (-. ph))))) ((/\ ch (-. ph)) (/\ ps ph) olc expcom ph (-> ps ch) pm2.21 com23 imp3a ch (-. ph) pm3.26 (-. ph) a1i jaod impbid)) thm (elimh () ((elimh.1 (-> (<-> ph (\/ (/\ ph ch) (/\ ps (-. ch)))) (<-> ch ta))) (elimh.2 (-> (<-> ps (\/ (/\ ph ch) (/\ ps (-. ch)))) (<-> th ta))) (elimh.3 th)) ta (ch ph ps dedlema elimh.1 syl ibi elimh.3 ch ps ph dedlemb elimh.2 syl mpbii pm2.61i)) thm (dedt () ((dedt.1 (-> (<-> ph (\/ (/\ ph ch) (/\ ps (-. ch)))) (<-> th ta))) (dedt.2 ta)) (-> ch th) (ch ph ps dedlema dedt.2 dedt.1 mpbiri syl)) thm (con3th () () (-> (-> ph ps) (-> (-. ps) (-. ph))) ((<-> ps (\/ (/\ ps (-> ph ps)) (/\ ph (-. (-> ph ps))))) id negbid (-. ph) imbi1d (<-> ps (\/ (/\ ps (-> ph ps)) (/\ ph (-. (-> ph ps))))) id ph imbi2d (<-> ph (\/ (/\ ps (-> ph ps)) (/\ ph (-. (-> ph ps))))) id ph imbi2d ph id elimh con3i dedt)) thm (consensus () () (<-> (\/ (\/ (/\ ph ps) (/\ (-. ph) ch)) (/\ ps ch)) (\/ (/\ ph ps) (/\ (-. ph) ch))) ((\/ (/\ ph ps) (/\ (-. ph) ch)) id ph ps ch dedlema biimpd ch adantrd ph ch ps dedlemb biimpd ps adantld pm2.61i ps ph ancom ch (-. ph) ancom orbi12i sylib jaoi (\/ (/\ ph ps) (/\ (-. ph) ch)) (/\ ps ch) orc impbi)) thm (pm4.42 () () (<-> ph (\/ (/\ ph ps) (/\ ph (-. ps)))) (ps ph ph dedlema ps ph ph dedlemb pm2.61i)) thm (ninba () ((ninba.1 ph)) (-> (-. ps) (<-> (-. ph) (/\ ch ps))) (ninba.1 ps ch niabn bicomd)) thm (prlem1 () ((prlem1.1 (-> ph (<-> et ch))) (prlem1.2 (-> ps (-. th)))) (-> ph (-> ps (-> (\/ (/\ ps ch) (/\ th ta)) et))) (prlem1.1 biimprcd ps adantl ps a1dd th et pm2.24 prlem1.2 syl5 ta adantr ph a1d jaoi com3l)) thm (prlem2 () () (<-> (\/ (/\ ph ps) (/\ ch th)) (/\ (\/ ph ch) (\/ (/\ ph ps) (/\ ch th)))) (ph ch orabs ps anbi1i (\/ ph ch) ph ps anass bitr ch ph orabs ch ph orcom ch anbi1i bitr th anbi1i (\/ ph ch) ch th anass bitr orbi12i (\/ ph ch) (/\ ph ps) (/\ ch th) andi bitr4)) thm (oplem1 () ((oplem1.1 (-> ph (\/ ps ch))) (oplem1.2 (-> ph (\/ th ta))) (oplem1.3 (<-> ps th)) (oplem1.4 (-> ch (<-> th ta)))) (-> ph ps) (oplem1.1 ord oplem1.2 ord oplem1.3 negbii syl5ib jcad oplem1.4 oplem1.3 syl5bb biimpar syl6 ps pm2.18 syl)) thm (rnlem () () (<-> (/\ (/\ ph ps) (/\ ch th)) (/\ (/\ (/\ ph ch) (/\ ps th)) (/\ (/\ ph th) (/\ ps ch)))) (ph ps (/\ ch th) anandir ph ch th anandi ps ch th anandi anbi12i (/\ ps ch) (/\ ps th) ancom (/\ (/\ ph ch) (/\ ph th)) anbi2i (/\ ph ch) (/\ ph th) (/\ ps th) (/\ ps ch) an4 bitr 3bitr)) thm (3orass () () (<-> (\/\/ ph ps ch) (\/ ph (\/ ps ch))) (ph ps ch df-3or ph ps ch orass bitr)) thm (3anass () () (<-> (/\/\ ph ps ch) (/\ ph (/\ ps ch))) (ph ps ch df-3an ph ps ch anass bitr)) thm (3anrot () () (<-> (/\/\ ph ps ch) (/\/\ ps ch ph)) (ph (/\ ps ch) ancom ph ps ch 3anass ps ch ph df-3an 3bitr4)) thm (3orrot () () (<-> (\/\/ ph ps ch) (\/\/ ps ch ph)) (ph (\/ ps ch) orcom ph ps ch 3orass ps ch ph df-3or 3bitr4)) thm (3ancoma () () (<-> (/\/\ ph ps ch) (/\/\ ps ph ch)) (ph ps ancom ch anbi1i ph ps ch df-3an ps ph ch df-3an 3bitr4)) thm (3ancomb () () (<-> (/\/\ ph ps ch) (/\/\ ph ch ps)) (ph ps ch 3ancoma ps ph ch 3anrot bitr)) thm (3anrev () () (<-> (/\/\ ph ps ch) (/\/\ ch ps ph)) (ph ps ch 3ancoma ch ps ph 3anrot bitr4)) thm (3simpa () () (-> (/\/\ ph ps ch) (/\ ph ps)) (ph ps ch df-3an pm3.26bd)) thm (3simpb () () (-> (/\/\ ph ps ch) (/\ ph ch)) (ph ps ch 3ancomb ph ch ps 3simpa sylbi)) thm (3simpc () () (-> (/\/\ ph ps ch) (/\ ps ch)) (ph ps ch 3anrot ps ch ph 3simpa sylbi)) thm (3simp1 () () (-> (/\/\ ph ps ch) ph) (ph ps ch 3simpa pm3.26d)) thm (3simp2 () () (-> (/\/\ ph ps ch) ps) (ph ps ch 3simpa pm3.27d)) thm (3simp3 () () (-> (/\/\ ph ps ch) ch) (ph ps ch 3simpc pm3.27d)) thm (3simp1i () ((3simp1i.1 (/\/\ ph ps ch))) ph (3simp1i.1 ph ps ch 3simp1 ax-mp)) thm (3simp2i () ((3simp1i.1 (/\/\ ph ps ch))) ps (3simp1i.1 ph ps ch 3simp2 ax-mp)) thm (3simp3i () ((3simp1i.1 (/\/\ ph ps ch))) ch (3simp1i.1 ph ps ch 3simp3 ax-mp)) thm (3simp1d () ((3simp1d.1 (-> ph (/\/\ ps ch th)))) (-> ph ps) (3simp1d.1 ps ch th 3simp1 syl)) thm (3simp2d () ((3simp1d.1 (-> ph (/\/\ ps ch th)))) (-> ph ch) (3simp1d.1 ps ch th 3simp2 syl)) thm (3simp3d () ((3simp1d.1 (-> ph (/\/\ ps ch th)))) (-> ph th) (3simp1d.1 ps ch th 3simp3 syl)) thm (3adant1 () ((3adant.1 (-> (/\ ph ps) ch))) (-> (/\/\ th ph ps) ch) (th ph ps 3simpc 3adant.1 syl)) thm (3adant2 () ((3adant.1 (-> (/\ ph ps) ch))) (-> (/\/\ ph th ps) ch) (ph th ps 3simpb 3adant.1 syl)) thm (3adant3 () ((3adant.1 (-> (/\ ph ps) ch))) (-> (/\/\ ph ps th) ch) (ph ps th 3simpa 3adant.1 syl)) thm (3ad2ant1 () ((3ad2ant.1 (-> ph ch))) (-> (/\/\ ph ps th) ch) (3ad2ant.1 th adantr ps 3adant2)) thm (3ad2ant2 () ((3ad2ant.1 (-> ph ch))) (-> (/\/\ ps ph th) ch) (3ad2ant.1 th adantr ps 3adant1)) thm (3ad2ant3 () ((3ad2ant.1 (-> ph ch))) (-> (/\/\ ps th ph) ch) (3ad2ant.1 th adantl ps 3adant1)) thm (3adantl1 () ((3adantl.1 (-> (/\ (/\ ph ps) ch) th))) (-> (/\ (/\/\ ta ph ps) ch) th) (3adantl.1 exp ta 3adant1 imp)) thm (3adantl2 () ((3adantl.1 (-> (/\ (/\ ph ps) ch) th))) (-> (/\ (/\/\ ph ta ps) ch) th) (3adantl.1 exp ta 3adant2 imp)) thm (3adantl3 () ((3adantl.1 (-> (/\ (/\ ph ps) ch) th))) (-> (/\ (/\/\ ph ps ta) ch) th) (3adantl.1 exp ta 3adant3 imp)) thm (3adantr1 () ((3adantr.1 (-> (/\ ph (/\ ps ch)) th))) (-> (/\ ph (/\/\ ta ps ch)) th) (3adantr.1 ancoms ta 3adantl1 ancoms)) thm (3adantr2 () ((3adantr.1 (-> (/\ ph (/\ ps ch)) th))) (-> (/\ ph (/\/\ ps ta ch)) th) (3adantr.1 ancoms ta 3adantl2 ancoms)) thm (3adantr3 () ((3adantr.1 (-> (/\ ph (/\ ps ch)) th))) (-> (/\ ph (/\/\ ps ch ta)) th) (3adantr.1 ancoms ta 3adantl3 ancoms)) thm (3mix1 () () (-> ph (\/\/ ph ps ch)) (ph (\/ ps ch) orc ph ps ch 3orass sylibr)) thm (3mix2 () () (-> ph (\/\/ ps ph ch)) (ph ch ps 3mix1 ps ph ch 3orrot sylibr)) thm (3mix3 () () (-> ph (\/\/ ps ch ph)) (ph ps ch 3mix1 ph ps ch 3orrot sylib)) thm (3pm3.2i () ((3pm3.2i.1 ph) (3pm3.2i.2 ps) (3pm3.2i.3 ch)) (/\/\ ph ps ch) (ph ps ch df-3an 3pm3.2i.1 3pm3.2i.2 pm3.2i 3pm3.2i.3 mpbir2an)) thm (3jca () ((3jca.1 (-> ph ps)) (3jca.2 (-> ph ch)) (3jca.3 (-> ph th))) (-> ph (/\/\ ps ch th)) (3jca.1 3jca.2 jca 3jca.3 jca ps ch th df-3an sylibr)) thm (3jcad () ((3jcad.1 (-> ph (-> ps ch))) (3jcad.2 (-> ph (-> ps th))) (3jcad.3 (-> ph (-> ps ta)))) (-> ph (-> ps (/\/\ ch th ta))) (3jcad.1 imp 3jcad.2 imp 3jcad.3 imp 3jca exp)) thm (3anim123i () ((3anim123i.1 (-> ph ps)) (3anim123i.2 (-> ch th)) (3anim123i.3 (-> ta et))) (-> (/\/\ ph ch ta) (/\/\ ps th et)) (3anim123i.1 3anim123i.2 anim12i 3anim123i.3 anim12i ph ch ta df-3an ps th et df-3an 3imtr4)) thm (3anbi123i () ((bi3.1 (<-> ph ps)) (bi3.2 (<-> ch th)) (bi3.3 (<-> ta et))) (<-> (/\/\ ph ch ta) (/\/\ ps th et)) (bi3.1 bi3.2 anbi12i bi3.3 anbi12i ph ch ta df-3an ps th et df-3an 3bitr4)) thm (3orbi123i () ((bi3.1 (<-> ph ps)) (bi3.2 (<-> ch th)) (bi3.3 (<-> ta et))) (<-> (\/\/ ph ch ta) (\/\/ ps th et)) (bi3.1 bi3.2 orbi12i bi3.3 orbi12i ph ch ta df-3or ps th et df-3or 3bitr4)) thm (3imp () ((3imp.1 (-> ph (-> ps (-> ch th))))) (-> (/\/\ ph ps ch) th) (ph ps ch df-3an 3imp.1 imp31 sylbi)) thm (3impa () ((3impa.1 (-> (/\ (/\ ph ps) ch) th))) (-> (/\/\ ph ps ch) th) (3impa.1 exp31 3imp)) thm (3impb () ((3impb.1 (-> (/\ ph (/\ ps ch)) th))) (-> (/\/\ ph ps ch) th) (3impb.1 exp32 3imp)) thm (3exp () ((3exp.1 (-> (/\/\ ph ps ch) th))) (-> ph (-> ps (-> ch th))) (ph ps ch df-3an 3exp.1 sylbir exp31)) thm (3expa () ((3exp.1 (-> (/\/\ ph ps ch) th))) (-> (/\ (/\ ph ps) ch) th) (3exp.1 3exp imp31)) thm (3expb () ((3exp.1 (-> (/\/\ ph ps ch) th))) (-> (/\ ph (/\ ps ch)) th) (3exp.1 3exp imp32)) thm (3com12 () ((3exp.1 (-> (/\/\ ph ps ch) th))) (-> (/\/\ ps ph ch) th) (3exp.1 3exp com12 3imp)) thm (3com13 () ((3exp.1 (-> (/\/\ ph ps ch) th))) (-> (/\/\ ch ps ph) th) (ch ps ph 3anrev 3exp.1 sylbi)) thm (3com23 () ((3exp.1 (-> (/\/\ ph ps ch) th))) (-> (/\/\ ph ch ps) th) (3exp.1 3exp com23 3imp)) thm (3coml () ((3exp.1 (-> (/\/\ ph ps ch) th))) (-> (/\/\ ps ch ph) th) (3exp.1 3com23 3com13)) thm (3comr () ((3exp.1 (-> (/\/\ ph ps ch) th))) (-> (/\/\ ch ph ps) th) (3exp.1 3coml 3coml)) thm (3imp1 () ((3imp1.1 (-> ph (-> ps (-> ch (-> th ta)))))) (-> (/\ (/\/\ ph ps ch) th) ta) (3imp1.1 3imp imp)) thm (3exp1 () ((3exp1.1 (-> (/\ (/\/\ ph ps ch) th) ta))) (-> ph (-> ps (-> ch (-> th ta)))) (3exp1.1 exp 3exp)) var (wff ze) thm (syl3an1 () ((syl3an.1 (-> (/\/\ ph ps ch) th)) (syl3an1.2 (-> ta ph))) (-> (/\/\ ta ps ch) th) (syl3an.1 3expb syl3an1.2 sylan 3impb)) thm (syl3an2 () ((syl3an.1 (-> (/\/\ ph ps ch) th)) (syl3an2.2 (-> ta ps))) (-> (/\/\ ph ta ch) th) (syl3an.1 3exp syl3an2.2 syl5 3imp)) thm (syl3an3 () ((syl3an.1 (-> (/\/\ ph ps ch) th)) (syl3an3.2 (-> ta ch))) (-> (/\/\ ph ps ta) th) (syl3an.1 3exp syl3an3.2 syl7 3imp)) thm (syl3an1b () ((syl3an.1 (-> (/\/\ ph ps ch) th)) (syl3an1b.2 (<-> ta ph))) (-> (/\/\ ta ps ch) th) (syl3an.1 syl3an1b.2 biimp syl3an1)) thm (syl3an2b () ((syl3an.1 (-> (/\/\ ph ps ch) th)) (syl3an2b.2 (<-> ta ps))) (-> (/\/\ ph ta ch) th) (syl3an.1 syl3an2b.2 biimp syl3an2)) thm (syl3an3b () ((syl3an.1 (-> (/\/\ ph ps ch) th)) (syl3an3b.2 (<-> ta ch))) (-> (/\/\ ph ps ta) th) (syl3an.1 syl3an3b.2 biimp syl3an3)) thm (syl3an1br () ((syl3an.1 (-> (/\/\ ph ps ch) th)) (syl3an1br.2 (<-> ph ta))) (-> (/\/\ ta ps ch) th) (syl3an.1 syl3an1br.2 biimpr syl3an1)) thm (syl3an2br () ((syl3an.1 (-> (/\/\ ph ps ch) th)) (syl3an2br.2 (<-> ps ta))) (-> (/\/\ ph ta ch) th) (syl3an.1 syl3an2br.2 biimpr syl3an2)) thm (syl3an3br () ((syl3an.1 (-> (/\/\ ph ps ch) th)) (syl3an3br.2 (<-> ch ta))) (-> (/\/\ ph ps ta) th) (syl3an.1 syl3an3br.2 biimpr syl3an3)) thm (syl3an () ((syl3an.1 (-> (/\/\ ph ps ch) th)) (syl3an.2 (-> ta ph)) (syl3an.3 (-> et ps)) (syl3an.4 (-> ze ch))) (-> (/\/\ ta et ze) th) (syl3an.2 syl3an.3 syl3an.4 3anim123i syl3an.1 syl)) thm (syl3anb () ((syl3an.1 (-> (/\/\ ph ps ch) th)) (syl3anb.2 (<-> ta ph)) (syl3anb.3 (<-> et ps)) (syl3anb.4 (<-> ze ch))) (-> (/\/\ ta et ze) th) (syl3anb.2 syl3anb.3 syl3anb.4 3anbi123i syl3an.1 sylbi)) thm (syl3anl1 () ((syl3anl1.1 (-> (/\ (/\/\ ph ps ch) th) ta)) (syl3an11.2 (-> et ph))) (-> (/\ (/\/\ et ps ch) th) ta) (syl3anl1.1 exp syl3an11.2 syl3an1 imp)) thm (syl3anl2 () ((syl3anl1.1 (-> (/\ (/\/\ ph ps ch) th) ta)) (syl3an12.2 (-> et ps))) (-> (/\ (/\/\ ph et ch) th) ta) (syl3anl1.1 exp syl3an12.2 syl3an2 imp)) thm (syl3anl3 () ((syl3anl1.1 (-> (/\ (/\/\ ph ps ch) th) ta)) (syl3an13.2 (-> et ch))) (-> (/\ (/\/\ ph ps et) th) ta) (syl3anl1.1 exp syl3an13.2 syl3an3 imp)) thm (syl3anc () ((syl3anc.1 (-> (/\/\ ph ps ch) th)) (syl3anc.2 (-> ta ph)) (syl3anc.3 (-> ta ps)) (syl3anc.4 (-> ta ch))) (-> ta th) (syl3anc.2 syl3anc.3 syl3anc.4 3jca syl3anc.1 syl)) thm (3impdi () ((3impdi.1 (-> (/\ (/\ ph ps) (/\ ph ch)) th))) (-> (/\/\ ph ps ch) th) (3impdi.1 anandis 3impb)) thm (3impdir () ((3impdir.1 (-> (/\ (/\ ph ps) (/\ ch ps)) th))) (-> (/\/\ ph ch ps) th) (3impdir.1 anandirs 3impa)) thm (3jao () () (-> (/\/\ (-> ph ps) (-> ch ps) (-> th ps)) (-> (\/\/ ph ch th) ps)) (ph ps ch jao (\/ ph ch) ps th jao syl6 3imp ph ch th df-3or syl5ib)) thm (3jaoi () ((3jaoi.1 (-> ph ps)) (3jaoi.2 (-> ch ps)) (3jaoi.3 (-> th ps))) (-> (\/\/ ph ch th) ps) (3jaoi.1 3jaoi.2 3jaoi.3 3pm3.2i ph ps ch th 3jao ax-mp)) thm (3jaod () ((3jaod.1 (-> ph (-> ps ch))) (3jaod.2 (-> ph (-> th ch))) (3jaod.3 (-> ph (-> ta ch)))) (-> ph (-> (\/\/ ps th ta) ch)) (ps ch th ta 3jao 3jaod.1 3jaod.2 3jaod.3 syl3anc)) thm (3jaoian () ((3jaoian.1 (-> (/\ ph ps) ch)) (3jaoian.2 (-> (/\ th ps) ch)) (3jaoian.3 (-> (/\ ta ps) ch))) (-> (/\ (\/\/ ph th ta) ps) ch) (3jaoian.1 exp 3jaoian.2 exp 3jaoian.3 exp 3jaoi imp)) thm (3jaodan () ((3jaodan.1 (-> (/\ ph ps) ch)) (3jaodan.2 (-> (/\ ph th) ch)) (3jaodan.3 (-> (/\ ph ta) ch))) (-> (/\ ph (\/\/ ps th ta)) ch) (3jaodan.1 exp 3jaodan.2 exp 3jaodan.3 exp 3jaod imp)) thm (syl3an9b () ((syl3an9b.1 (-> ph (<-> ps ch))) (syl3an9b.2 (-> th (<-> ch ta))) (syl3an9b.3 (-> et (<-> ta ze)))) (-> (/\/\ ph th et) (<-> ps ze)) (syl3an9b.1 syl3an9b.2 sylan9bb syl3an9b.3 sylan9bb 3impa)) thm (3orbi123d () ((bi3d.1 (-> ph (<-> ps ch))) (bi3d.2 (-> ph (<-> th ta))) (bi3d.3 (-> ph (<-> et ze)))) (-> ph (<-> (\/\/ ps th et) (\/\/ ch ta ze))) (bi3d.1 bi3d.2 orbi12d bi3d.3 orbi12d ps th et df-3or ch ta ze df-3or 3bitr4g)) thm (3anbi123d () ((bi3d.1 (-> ph (<-> ps ch))) (bi3d.2 (-> ph (<-> th ta))) (bi3d.3 (-> ph (<-> et ze)))) (-> ph (<-> (/\/\ ps th et) (/\/\ ch ta ze))) (bi3d.1 bi3d.2 anbi12d bi3d.3 anbi12d ps th et df-3an ch ta ze df-3an 3bitr4g)) thm (3anim123d () ((im3d.1 (-> ph (-> ps ch))) (im3d.2 (-> ph (-> th ta))) (im3d.3 (-> ph (-> et ze)))) (-> ph (-> (/\/\ ps th et) (/\/\ ch ta ze))) (im3d.1 im3d.2 anim12d im3d.3 anim12d ps th et df-3an ch ta ze df-3an 3imtr4g)) thm (3orim123d () ((im3d.1 (-> ph (-> ps ch))) (im3d.2 (-> ph (-> th ta))) (im3d.3 (-> ph (-> et ze)))) (-> ph (-> (\/\/ ps th et) (\/\/ ch ta ze))) (im3d.1 im3d.2 orim12d im3d.3 orim12d ps th et df-3or ch ta ze df-3or 3imtr4g)) thm (an6 () () (<-> (/\ (/\/\ ph ps ch) (/\/\ th ta et)) (/\/\ (/\ ph th) (/\ ps ta) (/\ ch et))) (ph ps ch df-3an th ta et df-3an anbi12i (/\ ph ps) ch (/\ th ta) et an4 ph ps th ta an4 (/\ ch et) anbi1i 3bitr (/\ ph th) (/\ ps ta) (/\ ch et) df-3an bitr4)) thm (mp3an1 () ((mp3an1.1 ph) (mp3an1.2 (-> (/\/\ ph ps ch) th))) (-> (/\ ps ch) th) (mp3an1.1 mp3an1.2 3expb mpan)) thm (mp3an2 () ((mp3an2.1 ps) (mp3an2.2 (-> (/\/\ ph ps ch) th))) (-> (/\ ph ch) th) (mp3an2.1 mp3an2.2 3expa mpanl2)) thm (mp3an3 () ((mp3an3.1 ch) (mp3an3.2 (-> (/\/\ ph ps ch) th))) (-> (/\ ph ps) th) (mp3an3.1 mp3an3.2 3expa mpan2)) thm (mp3an12 () ((mp3an12.1 ph) (mp3an12.2 ps) (mp3an12.3 (-> (/\/\ ph ps ch) th))) (-> ch th) (mp3an12.2 mp3an12.1 mp3an12.3 mp3an1 mpan)) thm (mp3an13 () ((mp3an13.1 ph) (mp3an13.2 ch) (mp3an13.3 (-> (/\/\ ph ps ch) th))) (-> ps th) (mp3an13.1 mp3an13.2 mp3an13.3 mp3an3 mpan)) thm (mp3an23 () ((mp3an23.1 ps) (mp3an23.2 ch) (mp3an23.3 (-> (/\/\ ph ps ch) th))) (-> ph th) (mp3an23.1 mp3an23.2 mp3an23.3 mp3an3 mpan2)) thm (mp3an1i () ((mp3an1i.1 ps) (mp3an1i.2 (-> ph (-> (/\/\ ps ch th) ta)))) (-> ph (-> (/\ ch th) ta)) (mp3an1i.1 mp3an1i.2 com12 mp3an1 com12)) thm (mp3anl1 () ((mp3anl1.1 ph) (mp3anl1.2 (-> (/\ (/\/\ ph ps ch) th) ta))) (-> (/\ (/\ ps ch) th) ta) (mp3anl1.1 mp3anl1.2 exp mp3an1 imp)) thm (mp3anl2 () ((mp3anl2.1 ps) (mp3anl2.2 (-> (/\ (/\/\ ph ps ch) th) ta))) (-> (/\ (/\ ph ch) th) ta) (mp3anl2.1 mp3anl2.2 exp mp3an2 imp)) thm (mp3anl3 () ((mp3anl3.1 ch) (mp3anl3.2 (-> (/\ (/\/\ ph ps ch) th) ta))) (-> (/\ (/\ ph ps) th) ta) (mp3anl3.1 mp3anl3.2 exp mp3an3 imp)) thm (mp3an () ((mp3an.1 ph) (mp3an.2 ps) (mp3an.3 ch) (mp3an.4 (-> (/\/\ ph ps ch) th))) th (mp3an.2 mp3an.3 mp3an.1 mp3an.4 mp3an1 mp2an)) thm (biimp3a () ((biimp3a.1 (-> (/\ ph ps) (<-> ch th)))) (-> (/\/\ ph ps ch) th) (biimp3a.1 biimpa 3impa)) thm (ecase23d () ((ecase23d.1 (-> ph (-. ch))) (ecase23d.2 (-> ph (-. th))) (ecase23d.3 (-> ph (\/\/ ps ch th)))) (-> ph ps) (ecase23d.1 ecase23d.2 jca ch th ioran sylibr ecase23d.3 ps ch th 3orass sylib ord mt3d)) thm (3ecase () ((3ecase.1 (-> (-. ph) th)) (3ecase.2 (-> (-. ps) th)) (3ecase.3 (-> (-. ch) th)) (3ecase.4 (-> (/\/\ ph ps ch) th))) th (3ecase.4 3exp 3ecase.1 ch a1d ps a1d pm2.61i 3ecase.2 3ecase.3 pm2.61nii)) thm (meredith () () (-> (-> (-> (-> (-> ph ps) (-> (-. ch) (-. th))) ch) ta) (-> (-> ta ph) (-> th ph))) (ch (-> (-. ch) (-> (-. ph) (-. th))) ax-3 ph ps pm2.21 (-> (-. ch) (-. th)) imim1i com23 syl5 ta imim1i con3d (-. ch) (-> (-. ph) (-. th)) pm2.27 impi com12 (-. ta) imim2d com12 a2d ta ph con3 syl5 ph th ax-3 syl6 syl)) thm (merlem1 () () (-> (-> (-> ch (-> (-. ph) ps)) ta) (-> ph ta)) ((-. ph) ps (-> (-. ta) (-. ch)) (-. (-> (-. ph) ps)) ta meredith (-> (-. ph) ps) (-> (-. (-> (-. ta) (-. ch))) (-. (-. (-> (-. ph) ps)))) ta ch (-> (-> ta (-. ph)) (-> (-. (-> (-. ph) ps)) (-. ph))) meredith ax-mp ta (-. ph) (-> (-. ph) ps) ph (-> ch (-> (-. ph) ps)) meredith ax-mp)) thm (merlem2 () () (-> (-> (-> ph ph) ch) (-> th ch)) ((-> ch ch) ph (-. th) ph merlem1 ch ch ph th (-> ph ph) meredith ax-mp)) thm (merlem3 () () (-> (-> (-> ps ch) ph) (-> ch ph)) ((-. ch) (-> (-. ch) (-. ch)) (-> ph ph) merlem2 (-> (-. ch) (-. ch)) (-> (-> ph ph) (-> (-. ch) (-. ch))) (-> (-> (-> ch ph) (-> (-. ps) (-. ps))) ps) merlem2 ax-mp ch ph ps ps (-> (-> ph ph) (-> (-. ch) (-. ch))) meredith ax-mp ph ph ch ch (-> ps ch) meredith ax-mp)) thm (merlem4 () () (-> ta (-> (-> ta ph) (-> th ph))) (ph ph th th ta meredith (-> (-> (-> ph ph) (-> (-. th) (-. th))) th) ta (-> (-> ta ph) (-> th ph)) merlem3 ax-mp)) thm (merlem5 () () (-> (-> ph ps) (-> (-. (-. ph)) ps)) (ps ps ps ps ps meredith ps ps ps (-. (-. ph)) ph meredith (-> ph ps) (-. ph) ps (-. (-> (-> (-> (-> (-> ps ps) (-> (-. ps) (-. ps))) ps) ps) (-> (-> ps ps) (-> ps ps)))) merlem1 (-> (-> (-> (-> ph ps) (-> (-. (-. ph)) ps)) (-. (-> (-> (-> (-> (-> ps ps) (-> (-. ps) (-. ps))) ps) ps) (-> (-> ps ps) (-> ps ps))))) (-> (-. ph) (-. (-> (-> (-> (-> (-> ps ps) (-> (-. ps) (-. ps))) ps) ps) (-> (-> ps ps) (-> ps ps)))))) ph (-> (-> (-> ps ps) (-> (-. ps) (-. (-. (-. ph))))) ps) merlem4 ax-mp (-> (-> ph ps) (-> (-. (-. ph)) ps)) (-. (-> (-> (-> (-> (-> ps ps) (-> (-. ps) (-. ps))) ps) ps) (-> (-> ps ps) (-> ps ps)))) ph (-> (-> (-> (-> (-> ps ps) (-> (-. ps) (-. ps))) ps) ps) (-> (-> ps ps) (-> ps ps))) (-> (-> (-> (-> ps ps) (-> (-. ps) (-. (-. (-. ph))))) ps) ph) meredith ax-mp ax-mp ax-mp)) thm (merlem6 () () (-> ch (-> (-> (-> ps ch) ph) (-> th ph))) ((-> ps ch) ph th merlem4 ps ch (-> (-> (-> ps ch) ph) (-> th ph)) merlem3 ax-mp)) thm (merlem7 () () (-> ph (-> (-> (-> ps ch) th) (-> (-> (-> ch ta) (-> (-. th) (-. ps))) th))) ((-> ps ch) th (-> (-> ch ta) (-> (-. th) (-. ps))) merlem4 (-> (-> (-> ch ta) (-> (-. th) (-. ps))) th) (-> (-> ps ch) th) (-. ph) (-. ch) merlem6 ch ta th ps (-> (-> (-> (-> (-> ps ch) th) (-> (-> (-> ch ta) (-> (-. th) (-. ps))) th)) (-. ph)) (-> (-. ch) (-. ph))) meredith ax-mp (-> (-> (-> ps ch) th) (-> (-> (-> ch ta) (-> (-. th) (-. ps))) th)) (-. ph) ch ph (-> ps ch) meredith ax-mp ax-mp)) thm (merlem8 () () (-> (-> (-> ps ch) th) (-> (-> (-> ch ta) (-> (-. th) (-. ps))) th)) (ph ph ph ph ph meredith (-> (-> (-> (-> (-> ph ph) (-> (-. ph) (-. ph))) ph) ph) (-> (-> ph ph) (-> ph ph))) ps ch th ta merlem7 ax-mp)) thm (merlem9 () () (-> (-> (-> ph ps) (-> ch (-> th (-> ps ta)))) (-> et (-> ch (-> th (-> ps ta))))) ((-> th (-> ps ta)) ch (-. et) (-. ps) merlem6 th (-> ps ta) (-> (-> (-> ch (-> th (-> ps ta))) (-. et)) (-> (-. ps) (-. et))) (-> (-. (-> (-. (-> (-> (-> ch (-> th (-> ps ta))) (-. et)) (-> (-. ps) (-. et)))) (-. th))) (-. ph)) merlem8 ax-mp ps ta (-> (-. (-> (-> (-> ch (-> th (-> ps ta))) (-. et)) (-> (-. ps) (-. et)))) (-. th)) ph (-> (-> (-> ch (-> th (-> ps ta))) (-. et)) (-> (-. ps) (-. et))) meredith ax-mp (-> ch (-> th (-> ps ta))) (-. et) ps et (-> ph ps) meredith ax-mp)) thm (merlem10 () () (-> (-> ph (-> ph ps)) (-> th (-> ph ps))) (ph ph ph ph ph meredith (-> ph ps) ph ph th ph meredith (-> (-> (-> (-> ph ps) ph) (-> (-. ph) (-. th))) ph) ph (-> ph (-> ph ps)) th ps (-> (-> (-> (-> (-> ph ph) (-> (-. ph) (-. ph))) ph) ph) (-> (-> ph ph) (-> ph ph))) merlem9 ax-mp ax-mp)) thm (merlem11 () () (-> (-> ph (-> ph ps)) (-> ph ps)) (ph ph ph ph ph meredith ph ps (-> ph (-> ph ps)) merlem10 (-> ph (-> ph ps)) (-> ph ps) (-> (-> (-> (-> (-> ph ph) (-> (-. ph) (-. ph))) ph) ph) (-> (-> ph ph) (-> ph ph))) merlem10 ax-mp ax-mp)) thm (merlem12 () () (-> (-> (-> th (-> (-. (-. ch)) ch)) ph) ph) (ch ch merlem5 ch (-> (-. (-. ch)) ch) th merlem2 ax-mp (-> th (-> (-. (-. ch)) ch)) ph (-> (-> th (-> (-. (-. ch)) ch)) ph) merlem4 ax-mp (-> (-> th (-> (-. (-. ch)) ch)) ph) ph merlem11 ax-mp)) thm (merlem13 () () (-> (-> ph ps) (-> (-> (-> th (-> (-. (-. ch)) ch)) (-. (-. ph))) ps)) (th ch (-. (-> (-> th (-> (-. (-. ch)) ch)) (-. (-. ph)))) merlem12 th ch (-. (-. ph)) merlem12 (-> (-> th (-> (-. (-. ch)) ch)) (-. (-. ph))) (-. (-. ph)) merlem5 ax-mp (-> (-. (-. (-> (-> th (-> (-. (-. ch)) ch)) (-. (-. ph))))) (-. (-. ph))) (-> (-. (-> (-> th (-> (-. (-. ch)) ch)) (-. (-. ph)))) ps) (-. (-> (-> th (-> (-. (-. ch)) ch)) (-. (-. ph)))) (-> th (-> (-. (-. ch)) ch)) merlem6 ax-mp (-. (-> (-> th (-> (-. (-. ch)) ch)) (-. (-. ph)))) ps (-. (-> (-> th (-> (-. (-. ch)) ch)) (-. (-. ph)))) (-. ph) (-> (-> th (-> (-. (-. ch)) ch)) (-. (-> (-> th (-> (-. (-. ch)) ch)) (-. (-. ph))))) meredith ax-mp ax-mp (-> (-. ph) (-. (-> (-> th (-> (-. (-. ch)) ch)) (-. (-. ph))))) (-> ps ps) ph (-> (-> (-> ps ps) (-> (-. ph) (-. (-> (-> th (-> (-. (-. ch)) ch)) (-. (-. ph)))))) ph) merlem6 ax-mp (-> (-> (-> ps ps) (-> (-. ph) (-. (-> (-> th (-> (-. (-. ch)) ch)) (-. (-. ph)))))) ph) ph merlem11 ax-mp ps ps ph (-> (-> th (-> (-. (-. ch)) ch)) (-. (-. ph))) ph meredith ax-mp)) thm (luk-1 () () (-> (-> ph ps) (-> (-> ps ch) (-> ph ch))) (ch ch (-. (-. ph)) ph ps meredith ph ps (-> ch ch) (-. ph) merlem13 (-> ph ps) (-> (-> (-> (-> ch ch) (-> (-. (-. (-. ph))) (-. ph))) (-. (-. ph))) ps) (-> (-> (-> ps ch) (-> ph ch)) ph) (-. (-> ph ps)) merlem13 ax-mp (-> (-> ps ch) (-> ph ch)) ph (-. (-. (-> ph ps))) (-> ph ps) (-> (-> (-> (-> ch ch) (-> (-. (-. (-. ph))) (-. ph))) (-. (-. ph))) ps) meredith ax-mp ax-mp)) thm (luk-2 () () (-> (-> (-. ph) ph) ph) (ph (-. (-> (-. ph) ph)) merlem5 (-> (-> ph (-. (-> (-. ph) ph))) (-> (-. (-. ph)) (-. (-> (-. ph) ph)))) (-. ph) (-> (-> (-> ph (-. (-> (-. ph) ph))) (-> (-. (-. ph)) (-. (-> (-. ph) ph)))) (-. ph)) merlem4 ax-mp (-> (-> (-> ph (-. (-> (-. ph) ph))) (-> (-. (-. ph)) (-. (-> (-. ph) ph)))) (-. ph)) (-. ph) merlem11 ax-mp ph (-. (-> (-. ph) ph)) (-. ph) (-> (-. ph) ph) (-. ph) meredith ax-mp (-> (-. ph) ph) ph merlem11 ax-mp)) thm (luk-3 () () (-> ph (-> (-. ph) ps)) ((-. ph) ps merlem11 (-. ph) ph ps (-> (-. ph) ps) merlem1 ax-mp)) thm (luklem1 () ((luklem1.1 (-> ph ps)) (luklem1.2 (-> ps ch))) (-> ph ch) (luklem1.2 luklem1.1 ph ps ch luk-1 ax-mp ax-mp)) thm (luklem2 () () (-> (-> ph (-. ps)) (-> (-> (-> ph ch) th) (-> ps th))) (ph (-. ps) ch luk-1 ps ch luk-3 ps (-> (-. ps) ch) (-> ph ch) luk-1 ax-mp luklem1 ps (-> ph ch) th luk-1 luklem1)) thm (luklem3 () () (-> ph (-> (-> (-> (-. ph) ps) ch) (-> th ch))) (ph (-. th) luk-3 (-. ph) th ps ch luklem2 luklem1)) thm (luklem4 () () (-> (-> (-> (-> (-. ph) ph) ph) ps) ps) ((-> (-> (-. ph) ph) ph) luk-2 ph luk-2 (-> (-> (-. ph) ph) ph) (-> (-> (-. ph) ph) ph) (-> (-> (-. ph) ph) ph) (-. ps) luklem3 ax-mp ax-mp (-. ps) (-> (-> (-. ph) ph) ph) ps luk-1 ax-mp ps luk-2 luklem1)) thm (luklem5 () () (-> ph (-> ps ph)) (ph ph ph ps luklem3 ph (-> ps ph) luklem4 luklem1)) thm (luklem6 () () (-> (-> ph (-> ph ps)) (-> ph ps)) (ph (-> ph ps) ps luk-1 (-. (-> ph ps)) (-. ps) luklem5 (-. ps) (-> ph ps) ps ps luklem2 ps (-> (-> ph ps) ps) luklem4 luklem1 luklem1 (-. (-> ph ps)) (-> (-> ph ps) ps) (-> ph ps) luk-1 ax-mp (-> (-> (-> ph ps) ps) (-> ph ps)) (-> (-. (-> ph ps)) (-> ph ps)) (-> ph ps) luk-1 ax-mp (-> ph ps) (-> (-> (-> (-> ph ps) ps) (-> ph ps)) (-> ph ps)) luklem4 ax-mp luklem1)) thm (luklem7 () () (-> (-> ph (-> ps ch)) (-> ps (-> ph ch))) (ph (-> ps ch) ch luk-1 ps (-> ps ch) luklem5 (-> ps ch) ps ch luk-1 luklem1 (-> ps ch) ch luklem6 luklem1 ps (-> (-> ps ch) ch) (-> ph ch) luk-1 ax-mp luklem1)) thm (luklem8 () () (-> (-> ph ps) (-> (-> ch ph) (-> ch ps))) (ch ph ps luk-1 (-> ch ph) (-> ph ps) (-> ch ps) luklem7 ax-mp)) thm (ax1 () () (-> ph (-> ps ph)) (ph ps luklem5)) thm (ax2 () () (-> (-> ph (-> ps ch)) (-> (-> ph ps) (-> ph ch))) (ph ps ch luklem7 ps (-> ph ch) ph luklem8 ph ch luklem6 (-> ph (-> ph ch)) (-> ph ch) (-> ph ps) luklem8 ax-mp luklem1 luklem1)) thm (ax3 () () (-> (-> (-. ph) (-. ps)) (-> ps ph)) ((-. ph) ps ph ph luklem2 ph (-> ps ph) luklem4 luklem1)) export (PROP-FULL pax/prop-full (PROP) "")