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. ) |
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. ) |