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 φ ψ φ ψ ψ φ