Metamath Proof Explorer

Theorem ifpbi23

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

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

Proof

Step Hyp Ref Expression
1 simpl ⊢ φ ↔ ψ ∧ χ ↔ θ → φ ↔ ψ
2 simpr ⊢ φ ↔ ψ ∧ χ ↔ θ → χ ↔ θ
3 1 2 ifpbi23d ⊢ φ ↔ ψ ∧ χ ↔ θ → if- τ φ χ ↔ if- τ ψ θ