Metamath Proof Explorer

Theorem ifpananb

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

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

Proof

Step	Hyp	Ref	Expression
1		anor	$⊢ (ψ \land χ) \leftrightarrow \neg (\neg ψ \lor \neg χ)$
2		anor	$⊢ (θ \land τ) \leftrightarrow \neg (\neg θ \lor \neg τ)$
3		ifpbi23	$⊢ (((ψ \land χ) \leftrightarrow \neg (\neg ψ \lor \neg χ)) \land ((θ \land τ) \leftrightarrow \neg (\neg θ \lor \neg τ))) \to (if- (φ, (ψ \land χ), (θ \land τ)) \leftrightarrow if- (φ, \neg (\neg ψ \lor \neg χ), \neg (\neg θ \lor \neg τ)))$
4	1 2 3	mp2an	$⊢ if- (φ, (ψ \land χ), (θ \land τ)) \leftrightarrow if- (φ, \neg (\neg ψ \lor \neg χ), \neg (\neg θ \lor \neg τ))$
5		ifpororb	$⊢ if- (φ, (\neg ψ \lor \neg χ), (\neg θ \lor \neg τ)) \leftrightarrow (if- (φ, \neg ψ, \neg θ) \lor if- (φ, \neg χ, \neg τ))$
6		ifpnotnotb	$⊢ if- (φ, \neg ψ, \neg θ) \leftrightarrow \neg if- (φ, ψ, θ)$
7		ifpnotnotb	$⊢ if- (φ, \neg χ, \neg τ) \leftrightarrow \neg if- (φ, χ, τ)$
8	6 7	orbi12i	$⊢ (if- (φ, \neg ψ, \neg θ) \lor if- (φ, \neg χ, \neg τ)) \leftrightarrow (\neg if- (φ, ψ, θ) \lor \neg if- (φ, χ, τ))$
9	5 8	bitri	$⊢ if- (φ, (\neg ψ \lor \neg χ), (\neg θ \lor \neg τ)) \leftrightarrow (\neg if- (φ, ψ, θ) \lor \neg if- (φ, χ, τ))$
10	9	notbii	$⊢ \neg if- (φ, (\neg ψ \lor \neg χ), (\neg θ \lor \neg τ)) \leftrightarrow \neg (\neg if- (φ, ψ, θ) \lor \neg if- (φ, χ, τ))$
11		ifpnotnotb	$⊢ if- (φ, \neg (\neg ψ \lor \neg χ), \neg (\neg θ \lor \neg τ)) \leftrightarrow \neg if- (φ, (\neg ψ \lor \neg χ), (\neg θ \lor \neg τ))$
12		anor	$⊢ (if- (φ, ψ, θ) \land if- (φ, χ, τ)) \leftrightarrow \neg (\neg if- (φ, ψ, θ) \lor \neg if- (φ, χ, τ))$
13	10 11 12	3bitr4i	$⊢ if- (φ, \neg (\neg ψ \lor \neg χ), \neg (\neg θ \lor \neg τ)) \leftrightarrow (if- (φ, ψ, θ) \land if- (φ, χ, τ))$
14	4 13	bitri	$⊢ if- (φ, (ψ \land χ), (θ \land τ)) \leftrightarrow (if- (φ, ψ, θ) \land if- (φ, χ, τ))$