Metamath Proof Explorer

Theorem aifftbifffaibifff

Description: Given a is equivalent to T., Given b is equivalent to F., there exists a proof for that a iff b is false. (Contributed by Jarvin Udandy, 7-Sep-2020)

Ref Expression
Hypotheses aifftbifffaibifff.1 ⊢ φ ↔ ⊤
aifftbifffaibifff.2 ⊢ ψ ↔ ⊥
Assertion aifftbifffaibifff ⊢ φ ↔ ψ ↔ ⊥

Proof

Step Hyp Ref Expression
1 aifftbifffaibifff.1 ⊢ φ ↔ ⊤
2 aifftbifffaibifff.2 ⊢ ψ ↔ ⊥
3 1 aistia ⊢ φ
4 2 aisfina ⊢ ¬ ψ
5 3 4 abnotbtaxb ⊢ φ ⊻ ψ
6 5 axorbtnotaiffb ⊢ ¬ φ ↔ ψ
7 nbfal ⊢ ¬ φ ↔ ψ ↔ φ ↔ ψ ↔ ⊥
8 7 biimpi ⊢ ¬ φ ↔ ψ → φ ↔ ψ ↔ ⊥
9 6 8 ax-mp ⊢ φ ↔ ψ ↔ ⊥