Metamath Proof Explorer

Theorem ifpbi123

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

Ref Expression
Assertion ifpbi123 ⊢ φ ↔ ψ ∧ χ ↔ θ ∧ τ ↔ η → if- φ χ τ ↔ if- ψ θ η

Proof

Step Hyp Ref Expression
1 simp1 ⊢ φ ↔ ψ ∧ χ ↔ θ ∧ τ ↔ η → φ ↔ ψ
2 simp2 ⊢ φ ↔ ψ ∧ χ ↔ θ ∧ τ ↔ η → χ ↔ θ
3 simp3 ⊢ φ ↔ ψ ∧ χ ↔ θ ∧ τ ↔ η → τ ↔ η
4 1 2 3 ifpbi123d ⊢ φ ↔ ψ ∧ χ ↔ θ ∧ τ ↔ η → if- φ χ τ ↔ if- ψ θ η