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 ) ) ) )