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-ψθη