Theorem anxordi 1479

Description: Conjunction distributes over exclusive-or. In intuitionistic logic this assertion is also true, even though xordi 937 does not necessarily hold, in part because the usual definition of xor is subtly different in intuitionistic logic. (Contributed by David A. Wheeler, 7-Oct-2018.)

Assertion

Ref	Expression
anxordi	|- ( ( ph /\ ( ps \/_ ch ) ) <-> ( ( ph /\ ps ) \/_ ( ph /\ ch ) ) )

Proof of Theorem anxordi

Step	Hyp	Ref	Expression
1		xordi 937	. 2 |- ( ( ph /\ -. ( ps <-> ch ) ) <-> -. ( ( ph /\ ps ) <-> ( ph /\ ch ) ) )
2		df-xor 1465	. . 3 |- ( ( ps \/_ ch ) <-> -. ( ps <-> ch ) )
3	2	anbi2i 730	. 2 |- ( ( ph /\ ( ps \/_ ch ) ) <-> ( ph /\ -. ( ps <-> ch ) ) )
4		df-xor 1465	. 2 |- ( ( ( ph /\ ps ) \/_ ( ph /\ ch ) ) <-> -. ( ( ph /\ ps ) <-> ( ph /\ ch ) ) )
5	1, 3, 4	3bitr4i 292	1 |- ( ( ph /\ ( ps \/_ ch ) ) <-> ( ( ph /\ ps ) \/_ ( ph /\ ch ) ) )

Syntax hints:   -. wn 3   <-> wb 196   /\ wa 384   \/_ wxo 1464

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386  df-xor 1465

This theorem is referenced by: (None)