Metamath Proof Explorer

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- φ χ τ