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

Metamath Proof Explorer

Theorem ifeq12

Description: Equality theorem for conditional operators. (Contributed by NM, 1-Sep-2004)

Ref Expression
Assertion ifeq12 ⊢ A = B ∧ C = D → if φ A C = if φ B D

Proof

Step Hyp Ref Expression
1 ifeq1 ⊢ A = B → if φ A C = if φ B C
2 ifeq2 ⊢ C = D → if φ B C = if φ B D
3 1 2 sylan9eq ⊢ A = B ∧ C = D → if φ A C = if φ B D