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	⊢ ( ( 𝜑 ↔ 𝜓 ) ↔ ( ( 𝜑 ⊼ 𝜓 ) ⊼ ( ( 𝜑 ⊼ 𝜑 ) ⊼ ( 𝜓 ⊼ 𝜓 ) ) ) )