bi2.04 Show Code edit
# There's no point in having this theorem if we're not going to prove it as
# described in prop.ghi.
#thm (dfbi1gb () () (<-> (<-> ph ps) (-. (-> (-> ph ps) (-. (-> ps ph)))))
# # No way! See the notes at http://us.metamath.org/mpegif/dfbi1gb.html
# ph ps dfbi1)
## Commute Antecedents
thm (bi2.04 () () (<-> (-> ph (-> ps ch)) (-> ps (-> ph ch)))
ph ps ch pm2.04
(-> (-> ph (-> ps ch)) (-> ps (-> ph ch)))
ps ph ch pm2.04
(-> (-> ps (-> ph ch)) (-> ph (-> ps ch)))
impbii)
(<-> (-> ph (-> ps ch)) (-> ps (-> ph ch)))
edit