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
|- ( ph <-> T. )
aifftbifffaibifff.2
|- ( ps <-> F. )
Assertion aifftbifffaibifff
|- ( ( ph <-> ps ) <-> F. )

Proof

Step Hyp Ref Expression
1 aifftbifffaibifff.1
 |-  ( ph <-> T. )
2 aifftbifffaibifff.2
 |-  ( ps <-> F. )
3 1 aistia
 |-  ph
4 2 aisfina
 |-  -. ps
5 3 4 abnotbtaxb
 |-  ( ph \/_ ps )
6 5 axorbtnotaiffb
 |-  -. ( ph <-> ps )
7 nbfal
 |-  ( -. ( ph <-> ps ) <-> ( ( ph <-> ps ) <-> F. ) )
8 7 biimpi
 |-  ( -. ( ph <-> ps ) -> ( ( ph <-> ps ) <-> F. ) )
9 6 8 ax-mp
 |-  ( ( ph <-> ps ) <-> F. )