Theorem tbw-bijust

Description: Justification for tbw-negdf . (Contributed by Anthony Hart, 15-Aug-2011) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	tbw-bijust	⊢ ( ( 𝜑 ↔ 𝜓 ) ↔ ( ( ( 𝜑 → 𝜓 ) → ( ( 𝜓 → 𝜑 ) → ⊥ ) ) → ⊥ ) )

Proof

Step	Hyp	Ref	Expression
1		dfbi1	⊢ ( ( 𝜑 ↔ 𝜓 ) ↔ ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) )
2		pm2.21	⊢ ( ¬ ( 𝜓 → 𝜑 ) → ( ( 𝜓 → 𝜑 ) → ⊥ ) )
3	2	imim2i	⊢ ( ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) → ( ( 𝜑 → 𝜓 ) → ( ( 𝜓 → 𝜑 ) → ⊥ ) ) )
4		id	⊢ ( ¬ ( 𝜓 → 𝜑 ) → ¬ ( 𝜓 → 𝜑 ) )
5		falim	⊢ ( ⊥ → ¬ ( 𝜓 → 𝜑 ) )
6	4 5	ja	⊢ ( ( ( 𝜓 → 𝜑 ) → ⊥ ) → ¬ ( 𝜓 → 𝜑 ) )
7	6	imim2i	⊢ ( ( ( 𝜑 → 𝜓 ) → ( ( 𝜓 → 𝜑 ) → ⊥ ) ) → ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) )
8	3 7	impbii	⊢ ( ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) ↔ ( ( 𝜑 → 𝜓 ) → ( ( 𝜓 → 𝜑 ) → ⊥ ) ) )
9	8	notbii	⊢ ( ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) ↔ ¬ ( ( 𝜑 → 𝜓 ) → ( ( 𝜓 → 𝜑 ) → ⊥ ) ) )
10		pm2.21	⊢ ( ¬ ( ( 𝜑 → 𝜓 ) → ( ( 𝜓 → 𝜑 ) → ⊥ ) ) → ( ( ( 𝜑 → 𝜓 ) → ( ( 𝜓 → 𝜑 ) → ⊥ ) ) → ⊥ ) )
11		ax-1	⊢ ( ¬ ( ( 𝜑 → 𝜓 ) → ( ( 𝜓 → 𝜑 ) → ⊥ ) ) → ( ( ( ( 𝜑 → 𝜓 ) → ( ( 𝜓 → 𝜑 ) → ⊥ ) ) → ⊥ ) → ¬ ( ( 𝜑 → 𝜓 ) → ( ( 𝜓 → 𝜑 ) → ⊥ ) ) ) )
12		falim	⊢ ( ⊥ → ( ( ( ( 𝜑 → 𝜓 ) → ( ( 𝜓 → 𝜑 ) → ⊥ ) ) → ⊥ ) → ¬ ( ( 𝜑 → 𝜓 ) → ( ( 𝜓 → 𝜑 ) → ⊥ ) ) ) )
13	11 12	ja	⊢ ( ( ( ( 𝜑 → 𝜓 ) → ( ( 𝜓 → 𝜑 ) → ⊥ ) ) → ⊥ ) → ( ( ( ( 𝜑 → 𝜓 ) → ( ( 𝜓 → 𝜑 ) → ⊥ ) ) → ⊥ ) → ¬ ( ( 𝜑 → 𝜓 ) → ( ( 𝜓 → 𝜑 ) → ⊥ ) ) ) )
14	13	pm2.43i	⊢ ( ( ( ( 𝜑 → 𝜓 ) → ( ( 𝜓 → 𝜑 ) → ⊥ ) ) → ⊥ ) → ¬ ( ( 𝜑 → 𝜓 ) → ( ( 𝜓 → 𝜑 ) → ⊥ ) ) )
15	10 14	impbii	⊢ ( ¬ ( ( 𝜑 → 𝜓 ) → ( ( 𝜓 → 𝜑 ) → ⊥ ) ) ↔ ( ( ( 𝜑 → 𝜓 ) → ( ( 𝜓 → 𝜑 ) → ⊥ ) ) → ⊥ ) )
16	1 9 15	3bitri	⊢ ( ( 𝜑 ↔ 𝜓 ) ↔ ( ( ( 𝜑 → 𝜓 ) → ( ( 𝜓 → 𝜑 ) → ⊥ ) ) → ⊥ ) )