Definition df-xor 1267

Description: Define exclusive disjunction (logical 'xor'). Return true if either the left or right, but not both, are true. Contrast with /\ (wa 97), \/ (wo 629), and -> (wi 4) . (Contributed by FL, 22-Nov-2010.) (Modified by Jim Kingdon, 1-Mar-2018.)

Assertion

Ref	Expression
df-xor	|- ( ( ph \/_ ps ) <-> ( ( ph \/ ps ) /\ -. ( ph /\ ps ) ) )

Detailed syntax breakdown of Definition df-xor

Step	Hyp	Ref	Expression
1		wph	. . 3 wff ph
2		wps	. . 3 wff ps
3	1, 2	wxo 1266	. 2 wff ( ph \/_ ps )
4	1, 2	wo 629	. . 3 wff ( ph \/ ps )
5	1, 2	wa 97	. . . 4 wff ( ph /\ ps )
6	5	wn 3	. . 3 wff -. ( ph /\ ps )
7	4, 6	wa 97	. 2 wff ( ( ph \/ ps ) /\ -. ( ph /\ ps ) )
8	3, 7	wb 98	1 wff ( ( ph \/_ ps ) <-> ( ( ph \/ ps ) /\ -. ( ph /\ ps ) ) )

This definition is referenced by:  xoranor  1268  xorbi2d  1271  xorbi1d  1272  xorbin  1275  xorcom  1279  xornbidc  1282  xordc1  1284  anxordi  1291  truxortru  1310  truxorfal  1311  falxortru  1312  falxorfal  1313  mptxor  1315  reapltxor  7580  bdxor  9956