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