Metamath Proof Explorer

Theorem ifpan123g

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

Ref Expression
Assertion ifpan123g ⊢ if- φ χ τ ∧ if- ψ θ η ↔ ¬ φ ∨ χ ∧ φ ∨ τ ∧ ¬ ψ ∨ θ ∧ ψ ∨ η

Proof

Step Hyp Ref Expression
1 dfifp4 ⊢ if- φ χ τ ↔ ¬ φ ∨ χ ∧ φ ∨ τ
2 dfifp4 ⊢ if- ψ θ η ↔ ¬ ψ ∨ θ ∧ ψ ∨ η
3 1 2 anbi12i ⊢ if- φ χ τ ∧ if- ψ θ η ↔ ¬ φ ∨ χ ∧ φ ∨ τ ∧ ¬ ψ ∨ θ ∧ ψ ∨ η