This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dfbi1

Description: Relate the biconditional connective to primitive connectives. See dfbi1ALT for an unusual version proved directly from axioms. (Contributed by NM, 29-Dec-1992)

Ref Expression
Assertion dfbi1 ( ( 𝜑 ↔ 𝜓 ) ↔ ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) )

Proof

Step Hyp Ref Expression
1 df-bi ⊢ ¬ ( ( ( 𝜑 ↔ 𝜓 ) → ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) ) → ¬ ( ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) → ( 𝜑 ↔ 𝜓 ) ) )
2 impbi ⊢ ( ( ( 𝜑 ↔ 𝜓 ) → ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) ) → ( ( ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( 𝜑 ↔ 𝜓 ) ↔ ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) ) ) )
3 2 con3rr3 ⊢ ( ¬ ( ( 𝜑 ↔ 𝜓 ) ↔ ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) ) → ( ( ( 𝜑 ↔ 𝜓 ) → ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) ) → ¬ ( ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) → ( 𝜑 ↔ 𝜓 ) ) ) )
4 1 3 mt3 ⊢ ( ( 𝜑 ↔ 𝜓 ) ↔ ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) )