Metamath Proof Explorer

Theorem ifpdfxor

Description: Define xor as conditional logic operator. (Contributed by RP, 20-Apr-2020)

Ref Expression
Assertion ifpdfxor 
|- ( ( ph \/_ ps ) <-> if- ( ph , -. ps , ps ) )

Proof

Step Hyp Ref Expression
1 xor2 
 |-  ( ( ph \/_ ps ) <-> ( ( ph \/ ps ) /\ -. ( ph /\ ps ) ) )
2 ifpdfor 
 |-  ( ( ph \/ ps ) <-> if- ( ph , T. , ps ) )
3 ifpnot23 
 |-  ( -. if- ( ph , ps , F. ) <-> if- ( ph , -. ps , -. F. ) )
4 ifpdfan 
 |-  ( ( ph /\ ps ) <-> if- ( ph , ps , F. ) )
5 3 4 xchnxbir 
 |-  ( -. ( ph /\ ps ) <-> if- ( ph , -. ps , -. F. ) )
6 2 5 anbi12i 
 |-  ( ( ( ph \/ ps ) /\ -. ( ph /\ ps ) ) <-> ( if- ( ph , T. , ps ) /\ if- ( ph , -. ps , -. F. ) ) )
7 ifpan23 
 |-  ( ( if- ( ph , T. , ps ) /\ if- ( ph , -. ps , -. F. ) ) <-> if- ( ph , ( T. /\ -. ps ) , ( ps /\ -. F. ) ) )
8 truan 
 |-  ( ( T. /\ -. ps ) <-> -. ps )
9 fal 
 |-  -. F.
10 9 biantru 
 |-  ( ps <-> ( ps /\ -. F. ) )
11 10 bicomi 
 |-  ( ( ps /\ -. F. ) <-> ps )
12 ifpbi23 
 |-  ( ( ( ( T. /\ -. ps ) <-> -. ps ) /\ ( ( ps /\ -. F. ) <-> ps ) ) -> ( if- ( ph , ( T. /\ -. ps ) , ( ps /\ -. F. ) ) <-> if- ( ph , -. ps , ps ) ) )
13 8 11 12 mp2an 
 |-  ( if- ( ph , ( T. /\ -. ps ) , ( ps /\ -. F. ) ) <-> if- ( ph , -. ps , ps ) )
14 7 13 bitri 
 |-  ( ( if- ( ph , T. , ps ) /\ if- ( ph , -. ps , -. F. ) ) <-> if- ( ph , -. ps , ps ) )
15 1 6 14 3bitri 
 |-  ( ( ph \/_ ps ) <-> if- ( ph , -. ps , ps ) )