Description: Given a is equivalent to (not b), c is equivalent to a, there exists a proof for ( not ( c iff b ) ). (Contributed by Jarvin Udandy, 7-Sep-2016)
Ref | Expression | ||
---|---|---|---|
Hypotheses | aiffnbandciffatnotciffb.1 | |- ( ph <-> -. ps ) |
|
aiffnbandciffatnotciffb.2 | |- ( ch <-> ph ) |
||
Assertion | aiffnbandciffatnotciffb | |- -. ( ch <-> ps ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | aiffnbandciffatnotciffb.1 | |- ( ph <-> -. ps ) |
|
2 | aiffnbandciffatnotciffb.2 | |- ( ch <-> ph ) |
|
3 | 2 1 | bitri | |- ( ch <-> -. ps ) |
4 | xor3 | |- ( -. ( ch <-> ps ) <-> ( ch <-> -. ps ) ) |
|
5 | 3 4 | mpbir | |- -. ( ch <-> ps ) |