ifpan23

Description: Conjunction of conditional logical operators. (Contributed by RP, 20-Apr-2020)

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

Step	Hyp	Ref	Expression
1		ifpan123g	$⊢ (if- (φ, ψ, χ) \land if- (φ, θ, τ)) \leftrightarrow (((\neg φ \lor ψ) \land (φ \lor χ)) \land ((\neg φ \lor θ) \land (φ \lor τ)))$
2		an4	$⊢ (((\neg φ \lor ψ) \land (φ \lor χ)) \land ((\neg φ \lor θ) \land (φ \lor τ))) \leftrightarrow (((\neg φ \lor ψ) \land (\neg φ \lor θ)) \land ((φ \lor χ) \land (φ \lor τ)))$
3		dfifp4	$⊢ if- (φ, (ψ \land θ), (χ \land τ)) \leftrightarrow ((\neg φ \lor (ψ \land θ)) \land (φ \lor (χ \land τ)))$
4		ordi	$⊢ (\neg φ \lor (ψ \land θ)) \leftrightarrow ((\neg φ \lor ψ) \land (\neg φ \lor θ))$
5		ordi	$⊢ (φ \lor (χ \land τ)) \leftrightarrow ((φ \lor χ) \land (φ \lor τ))$
6	4 5	anbi12i	$⊢ ((\neg φ \lor (ψ \land θ)) \land (φ \lor (χ \land τ))) \leftrightarrow (((\neg φ \lor ψ) \land (\neg φ \lor θ)) \land ((φ \lor χ) \land (φ \lor τ)))$
7	3 6	bitr2i	$⊢ (((\neg φ \lor ψ) \land (\neg φ \lor θ)) \land ((φ \lor χ) \land (φ \lor τ))) \leftrightarrow if- (φ, (ψ \land θ), (χ \land τ))$
8	1 2 7	3bitri	$⊢ (if- (φ, ψ, χ) \land if- (φ, θ, τ)) \leftrightarrow if- (φ, (ψ \land θ), (χ \land τ))$

Metamath Proof Explorer