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

Metamath Proof Explorer

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