Metamath Proof Explorer

Theorem ifpan23

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

Ref Expression
Assertion ifpan23 ⊢ if- φ ψ χ ∧ if- φ θ τ ↔ if- φ ψ ∧ θ χ ∧ τ

Proof

Step Hyp Ref Expression
1 ifpan123g ⊢ if- φ ψ χ ∧ if- φ θ τ ↔ ¬ φ ∨ ψ ∧ φ ∨ χ ∧ ¬ φ ∨ θ ∧ φ ∨ τ
2 an4 ⊢ ¬ φ ∨ ψ ∧ φ ∨ χ ∧ ¬ φ ∨ θ ∧ φ ∨ τ ↔ ¬ φ ∨ ψ ∧ ¬ φ ∨ θ ∧ φ ∨ χ ∧ φ ∨ τ
3 dfifp4 ⊢ if- φ ψ ∧ θ χ ∧ τ ↔ ¬ φ ∨ ψ ∧ θ ∧ φ ∨ χ ∧ τ
4 ordi ⊢ ¬ φ ∨ ψ ∧ θ ↔ ¬ φ ∨ ψ ∧ ¬ φ ∨ θ
5 ordi ⊢ φ ∨ χ ∧ τ ↔ φ ∨ χ ∧ φ ∨ τ
6 4 5 anbi12i ⊢ ¬ φ ∨ ψ ∧ θ ∧ φ ∨ χ ∧ τ ↔ ¬ φ ∨ ψ ∧ ¬ φ ∨ θ ∧ φ ∨ χ ∧ φ ∨ τ
7 3 6 bitr2i ⊢ ¬ φ ∨ ψ ∧ ¬ φ ∨ θ ∧ φ ∨ χ ∧ φ ∨ τ ↔ if- φ ψ ∧ θ χ ∧ τ
8 1 2 7 3bitri ⊢ if- φ ψ χ ∧ if- φ θ τ ↔ if- φ ψ ∧ θ χ ∧ τ