Theorem ifpxorxorb

Description: Factor conditional logic operator over xor in terms 2 and 3. (Contributed by RP, 21-Apr-2020)

	Ref	Expression
Assertion	ifpxorxorb	⊢ ( if- ( 𝜑 , ( 𝜓 ⊻ 𝜒 ) , ( 𝜃 ⊻ 𝜏 ) ) ↔ ( if- ( 𝜑 , 𝜓 , 𝜃 ) ⊻ if- ( 𝜑 , 𝜒 , 𝜏 ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-xor	⊢ ( ( 𝜓 ⊻ 𝜒 ) ↔ ¬ ( 𝜓 ↔ 𝜒 ) )
2		df-xor	⊢ ( ( 𝜃 ⊻ 𝜏 ) ↔ ¬ ( 𝜃 ↔ 𝜏 ) )
3		ifpbi23	⊢ ( ( ( ( 𝜓 ⊻ 𝜒 ) ↔ ¬ ( 𝜓 ↔ 𝜒 ) ) ∧ ( ( 𝜃 ⊻ 𝜏 ) ↔ ¬ ( 𝜃 ↔ 𝜏 ) ) ) → ( if- ( 𝜑 , ( 𝜓 ⊻ 𝜒 ) , ( 𝜃 ⊻ 𝜏 ) ) ↔ if- ( 𝜑 , ¬ ( 𝜓 ↔ 𝜒 ) , ¬ ( 𝜃 ↔ 𝜏 ) ) ) )
4	1 2 3	mp2an	⊢ ( if- ( 𝜑 , ( 𝜓 ⊻ 𝜒 ) , ( 𝜃 ⊻ 𝜏 ) ) ↔ if- ( 𝜑 , ¬ ( 𝜓 ↔ 𝜒 ) , ¬ ( 𝜃 ↔ 𝜏 ) ) )
5		ifpbibib	⊢ ( if- ( 𝜑 , ( 𝜓 ↔ 𝜒 ) , ( 𝜃 ↔ 𝜏 ) ) ↔ ( if- ( 𝜑 , 𝜓 , 𝜃 ) ↔ if- ( 𝜑 , 𝜒 , 𝜏 ) ) )
6	5	notbii	⊢ ( ¬ if- ( 𝜑 , ( 𝜓 ↔ 𝜒 ) , ( 𝜃 ↔ 𝜏 ) ) ↔ ¬ ( if- ( 𝜑 , 𝜓 , 𝜃 ) ↔ if- ( 𝜑 , 𝜒 , 𝜏 ) ) )
7		ifpnotnotb	⊢ ( if- ( 𝜑 , ¬ ( 𝜓 ↔ 𝜒 ) , ¬ ( 𝜃 ↔ 𝜏 ) ) ↔ ¬ if- ( 𝜑 , ( 𝜓 ↔ 𝜒 ) , ( 𝜃 ↔ 𝜏 ) ) )
8		df-xor	⊢ ( ( if- ( 𝜑 , 𝜓 , 𝜃 ) ⊻ if- ( 𝜑 , 𝜒 , 𝜏 ) ) ↔ ¬ ( if- ( 𝜑 , 𝜓 , 𝜃 ) ↔ if- ( 𝜑 , 𝜒 , 𝜏 ) ) )
9	6 7 8	3bitr4i	⊢ ( if- ( 𝜑 , ¬ ( 𝜓 ↔ 𝜒 ) , ¬ ( 𝜃 ↔ 𝜏 ) ) ↔ ( if- ( 𝜑 , 𝜓 , 𝜃 ) ⊻ if- ( 𝜑 , 𝜒 , 𝜏 ) ) )
10	4 9	bitri	⊢ ( if- ( 𝜑 , ( 𝜓 ⊻ 𝜒 ) , ( 𝜃 ⊻ 𝜏 ) ) ↔ ( if- ( 𝜑 , 𝜓 , 𝜃 ) ⊻ if- ( 𝜑 , 𝜒 , 𝜏 ) ) )