This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ifbieq12d2

Description: Equivalence deduction for conditional operators. (Contributed by Thierry Arnoux, 14-Feb-2017) (Proof shortened by Wolf Lammen, 24-Jun-2021)

Ref Expression
Hypotheses ifbieq12d2.1 ⊢ φ → ψ ↔ χ
ifbieq12d2.2 ⊢ φ ∧ ψ → A = C
ifbieq12d2.3 ⊢ φ ∧ ¬ ψ → B = D
Assertion ifbieq12d2 ⊢ φ → if ψ A B = if χ C D

Proof

Step Hyp Ref Expression
1 ifbieq12d2.1 ⊢ φ → ψ ↔ χ
2 ifbieq12d2.2 ⊢ φ ∧ ψ → A = C
3 ifbieq12d2.3 ⊢ φ ∧ ¬ ψ → B = D
4 2 3 ifeq12da ⊢ φ → if ψ A B = if ψ C D
5 1 ifbid ⊢ φ → if ψ C D = if χ C D
6 4 5 eqtrd ⊢ φ → if ψ A B = if χ C D