Theorem anxordi 1527

Description: Conjunction distributes over exclusive-or. In intuitionistic logic this assertion is also true, even though xordi 1018 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	⊢ ((𝜑 ∧ (𝜓 ⊻ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ⊻ (𝜑 ∧ 𝜒)))

Proof of Theorem anxordi

Step	Hyp	Ref	Expression
1		xordi 1018	. 2 ⊢ ((𝜑 ∧ ¬ (𝜓 ↔ 𝜒)) ↔ ¬ ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ 𝜒)))
2		df-xor 1513	. . 3 ⊢ ((𝜓 ⊻ 𝜒) ↔ ¬ (𝜓 ↔ 𝜒))
3	2	anbi2i 623	. 2 ⊢ ((𝜑 ∧ (𝜓 ⊻ 𝜒)) ↔ (𝜑 ∧ ¬ (𝜓 ↔ 𝜒)))
4		df-xor 1513	. 2 ⊢ (((𝜑 ∧ 𝜓) ⊻ (𝜑 ∧ 𝜒)) ↔ ¬ ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ 𝜒)))
5	1, 3, 4	3bitr4i 303	1 ⊢ ((𝜑 ∧ (𝜓 ⊻ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ⊻ (𝜑 ∧ 𝜒)))

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395   ⊻ wxo 1512

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 207  df-an 396  df-xor 1513

This theorem is referenced by: (None)