Metamath Proof Explorer


Theorem bijust

Description: Theorem used to justify the definition of the biconditional df-bi . Instance of bijust0 . (Contributed by NM, 11-May-1999)

Ref Expression
Assertion bijust
|- -. ( ( -. ( ( ph -> ps ) -> -. ( ps -> ph ) ) -> -. ( ( ph -> ps ) -> -. ( ps -> ph ) ) ) -> -. ( -. ( ( ph -> ps ) -> -. ( ps -> ph ) ) -> -. ( ( ph -> ps ) -> -. ( ps -> ph ) ) ) )

Proof

Step Hyp Ref Expression
1 bijust0
 |-  -. ( ( -. ( ( ph -> ps ) -> -. ( ps -> ph ) ) -> -. ( ( ph -> ps ) -> -. ( ps -> ph ) ) ) -> -. ( -. ( ( ph -> ps ) -> -. ( ps -> ph ) ) -> -. ( ( ph -> ps ) -> -. ( ps -> ph ) ) ) )