Metamath Proof Explorer

Theorem ifpbi1

Description: Equivalence theorem for conditional logical operators. (Contributed by RP, 14-Apr-2020)

Ref Expression
Assertion ifpbi1 ⊢ φ ↔ ψ → if- φ χ θ ↔ if- ψ χ θ

Proof

Step Hyp Ref Expression
1 imbi1 ⊢ φ ↔ ψ → φ → χ ↔ ψ → χ
2 notbi ⊢ φ ↔ ψ ↔ ¬ φ ↔ ¬ ψ
3 2 biimpi ⊢ φ ↔ ψ → ¬ φ ↔ ¬ ψ
4 3 imbi1d ⊢ φ ↔ ψ → ¬ φ → θ ↔ ¬ ψ → θ
5 1 4 anbi12d ⊢ φ ↔ ψ → φ → χ ∧ ¬ φ → θ ↔ ψ → χ ∧ ¬ ψ → θ
6 dfifp2 ⊢ if- φ χ θ ↔ φ → χ ∧ ¬ φ → θ
7 dfifp2 ⊢ if- ψ χ θ ↔ ψ → χ ∧ ¬ ψ → θ
8 5 6 7 3bitr4g ⊢ φ ↔ ψ → if- φ χ θ ↔ if- ψ χ θ