Metamath Proof Explorer


Theorem aiffnbandciffatnotciffb

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 )

Proof

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 )