Theorem tbw-bijust 1702

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

Assertion

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

Proof of Theorem tbw-bijust

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205  ⊥wfal 1551

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206  df-tru 1542  df-fal 1552

This theorem is referenced by:  tbw-negdf  1703