Metamath Proof Explorer

Theorem ifpbi123d

Description: Equivalence deduction for conditional operator for propositions. (Contributed by AV, 30-Dec-2020) (Proof shortened by Wolf Lammen, 17-Apr-2024)

Ref Expression
Hypotheses ifpbi123d.1 ⊢ φ → ψ ↔ τ
ifpbi123d.2 ⊢ φ → χ ↔ η
ifpbi123d.3 ⊢ φ → θ ↔ ζ
Assertion ifpbi123d ⊢ φ → if- ψ χ θ ↔ if- τ η ζ

Proof

Step Hyp Ref Expression
1 ifpbi123d.1 ⊢ φ → ψ ↔ τ
2 ifpbi123d.2 ⊢ φ → χ ↔ η
3 ifpbi123d.3 ⊢ φ → θ ↔ ζ
4 1 2 imbi12d ⊢ φ → ψ → χ ↔ τ → η
5 1 3 orbi12d ⊢ φ → ψ ∨ θ ↔ τ ∨ ζ
6 4 5 anbi12d ⊢ φ → ψ → χ ∧ ψ ∨ θ ↔ τ → η ∧ τ ∨ ζ
7 dfifp3 ⊢ if- ψ χ θ ↔ ψ → χ ∧ ψ ∨ θ
8 dfifp3 ⊢ if- τ η ζ ↔ τ → η ∧ τ ∨ ζ
9 6 7 8 3bitr4g ⊢ φ → if- ψ χ θ ↔ if- τ η ζ