oplem1 Show Code edit
# A specialized lemma for set theory (ordered pair theorem).
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 notbii syl5ib jcad oplem1.4 oplem1.3 syl5bb biimpar syl6 ps pm2.18 syl)
(-> ph ps)
edit