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