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

Metamath Proof Explorer

Theorem nanbi

Description: Biconditional in terms of alternative denial. (Contributed by Jeff Hoffman, 19-Nov-2007) (Proof shortened by Wolf Lammen, 27-Jun-2020)

Ref Expression
Assertion nanbi ( ( 𝜑 ↔ 𝜓 ) ↔ ( ( 𝜑 ⊼ 𝜓 ) ⊼ ( ( 𝜑 ⊼ 𝜑 ) ⊼ ( 𝜓 ⊼ 𝜓 ) ) ) )

Proof

Step Hyp Ref Expression
1 dfbi3 ⊢ ( ( 𝜑 ↔ 𝜓 ) ↔ ( ( 𝜑 ∧ 𝜓 ) ∨ ( ¬ 𝜑 ∧ ¬ 𝜓 ) ) )
2 df-or ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∨ ( ¬ 𝜑 ∧ ¬ 𝜓 ) ) ↔ ( ¬ ( 𝜑 ∧ 𝜓 ) → ( ¬ 𝜑 ∧ ¬ 𝜓 ) ) )
3 df-nan ⊢ ( ( 𝜑 ⊼ 𝜓 ) ↔ ¬ ( 𝜑 ∧ 𝜓 ) )
4 3 bicomi ⊢ ( ¬ ( 𝜑 ∧ 𝜓 ) ↔ ( 𝜑 ⊼ 𝜓 ) )
5 nannot ⊢ ( ¬ 𝜑 ↔ ( 𝜑 ⊼ 𝜑 ) )
6 nannot ⊢ ( ¬ 𝜓 ↔ ( 𝜓 ⊼ 𝜓 ) )
7 5 6 anbi12i ⊢ ( ( ¬ 𝜑 ∧ ¬ 𝜓 ) ↔ ( ( 𝜑 ⊼ 𝜑 ) ∧ ( 𝜓 ⊼ 𝜓 ) ) )
8 4 7 imbi12i ⊢ ( ( ¬ ( 𝜑 ∧ 𝜓 ) → ( ¬ 𝜑 ∧ ¬ 𝜓 ) ) ↔ ( ( 𝜑 ⊼ 𝜓 ) → ( ( 𝜑 ⊼ 𝜑 ) ∧ ( 𝜓 ⊼ 𝜓 ) ) ) )
9 1 2 8 3bitri ⊢ ( ( 𝜑 ↔ 𝜓 ) ↔ ( ( 𝜑 ⊼ 𝜓 ) → ( ( 𝜑 ⊼ 𝜑 ) ∧ ( 𝜓 ⊼ 𝜓 ) ) ) )
10 nannan ⊢ ( ( ( 𝜑 ⊼ 𝜓 ) ⊼ ( ( 𝜑 ⊼ 𝜑 ) ⊼ ( 𝜓 ⊼ 𝜓 ) ) ) ↔ ( ( 𝜑 ⊼ 𝜓 ) → ( ( 𝜑 ⊼ 𝜑 ) ∧ ( 𝜓 ⊼ 𝜓 ) ) ) )
11 9 10 bitr4i ⊢ ( ( 𝜑 ↔ 𝜓 ) ↔ ( ( 𝜑 ⊼ 𝜓 ) ⊼ ( ( 𝜑 ⊼ 𝜑 ) ⊼ ( 𝜓 ⊼ 𝜓 ) ) ) )