Metamath Proof Explorer

Theorem ifpan123g

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

		Ref	Expression
	Assertion	ifpan123g	$⊢ (if- (φ, χ, τ) \land if- (ψ, θ, η)) \leftrightarrow (((\neg φ \lor χ) \land (φ \lor τ)) \land ((\neg ψ \lor θ) \land (ψ \lor η)))$

Step	Hyp	Ref	Expression
1		dfifp4	$⊢ if- (φ, χ, τ) \leftrightarrow ((\neg φ \lor χ) \land (φ \lor τ))$
2		dfifp4	$⊢ if- (ψ, θ, η) \leftrightarrow ((\neg ψ \lor θ) \land (ψ \lor η))$
3	1 2	anbi12i	$⊢ (if- (φ, χ, τ) \land if- (ψ, θ, η)) \leftrightarrow (((\neg φ \lor χ) \land (φ \lor τ)) \land ((\neg ψ \lor θ) \land (ψ \lor η)))$