Theorem anxordi

Description: Conjunction distributes over exclusive-or. In intuitionistic logic this assertion is also true, even though xordi 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)

	Ref	Expression
Assertion	anxordi	⊢ ( ( 𝜑 ∧ ( 𝜓 ⊻ 𝜒 ) ) ↔ ( ( 𝜑 ∧ 𝜓 ) ⊻ ( 𝜑 ∧ 𝜒 ) ) )

Proof

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