ifpxorxorb

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

		Ref	Expression
	Assertion	ifpxorxorb	$⊢ if- (φ, (ψ ⊻ χ), (θ ⊻ τ)) \leftrightarrow (if- (φ, ψ, θ) ⊻ if- (φ, χ, τ))$

Step	Hyp	Ref	Expression
1		df-xor	$⊢ (ψ ⊻ χ) \leftrightarrow \neg (ψ \leftrightarrow χ)$
2		df-xor	$⊢ (θ ⊻ τ) \leftrightarrow \neg (θ \leftrightarrow τ)$
3		ifpbi23	$⊢ (((ψ ⊻ χ) \leftrightarrow \neg (ψ \leftrightarrow χ)) \land ((θ ⊻ τ) \leftrightarrow \neg (θ \leftrightarrow τ))) \to (if- (φ, (ψ ⊻ χ), (θ ⊻ τ)) \leftrightarrow if- (φ, \neg (ψ \leftrightarrow χ), \neg (θ \leftrightarrow τ)))$
4	1 2 3	mp2an	$⊢ if- (φ, (ψ ⊻ χ), (θ ⊻ τ)) \leftrightarrow if- (φ, \neg (ψ \leftrightarrow χ), \neg (θ \leftrightarrow τ))$
5		ifpbibib	$⊢ if- (φ, (ψ \leftrightarrow χ), (θ \leftrightarrow τ)) \leftrightarrow (if- (φ, ψ, θ) \leftrightarrow if- (φ, χ, τ))$
6	5	notbii	$⊢ \neg if- (φ, (ψ \leftrightarrow χ), (θ \leftrightarrow τ)) \leftrightarrow \neg (if- (φ, ψ, θ) \leftrightarrow if- (φ, χ, τ))$
7		ifpnotnotb	$⊢ if- (φ, \neg (ψ \leftrightarrow χ), \neg (θ \leftrightarrow τ)) \leftrightarrow \neg if- (φ, (ψ \leftrightarrow χ), (θ \leftrightarrow τ))$
8		df-xor	$⊢ (if- (φ, ψ, θ) ⊻ if- (φ, χ, τ)) \leftrightarrow \neg (if- (φ, ψ, θ) \leftrightarrow if- (φ, χ, τ))$
9	6 7 8	3bitr4i	$⊢ if- (φ, \neg (ψ \leftrightarrow χ), \neg (θ \leftrightarrow τ)) \leftrightarrow (if- (φ, ψ, θ) ⊻ if- (φ, χ, τ))$
10	4 9	bitri	$⊢ if- (φ, (ψ ⊻ χ), (θ ⊻ τ)) \leftrightarrow (if- (φ, ψ, θ) ⊻ if- (φ, χ, τ))$

Metamath Proof Explorer