Theorem ifeq2d 4298

Description: Equality deduction for conditional operator. (Contributed by NM, 16-Feb-2005.)

Hypothesis

Ref	Expression
ifeq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
ifeq2d	⊢ (𝜑 → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵))

Proof of Theorem ifeq2d

Step	Hyp	Ref	Expression
1		ifeq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		ifeq2 4284	. 2 ⊢ (𝐴 = 𝐵 → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵))
3	1, 2	syl 17	1 ⊢ (𝜑 → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵))

Syntax hints:   → wi 4   = wceq 1637  ifcif 4279

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-rab 3105  df-v 3393  df-un 3774  df-if 4280

This theorem is referenced by:  ifeq12d  4299  ifbieq2d  4304  ifeq2da  4310  ifcomnan  4333  rdgeq1  7739  cantnflem1d  8828  cantnflem1  8829  rexmul  12315  1arithlem4  15843  ramcl  15946  mplcoe1  19670  mplcoe5  19673  subrgascl  19702  scmatscm  20527  marrepfval  20574  ma1repveval  20585  mulmarep1el  20586  mdetralt2  20623  mdetunilem8  20633  maduval  20652  maducoeval2  20654  madurid  20658  minmar1val0  20661  monmatcollpw  20794  pmatcollpwscmatlem1  20804  monmat2matmon  20839  itg2monolem1  23730  iblmulc2  23810  itgmulc2lem1  23811  bddmulibl  23818  dvtaylp  24337  dchrinvcl  25191  rpvmasum2  25414  padicfval  25518  plymulx  30949  itg2addnclem  33771  itg2addnclem3  33773  itg2addnc  33774  itgmulc2nclem1  33786  hdmap1fval  37574  itgioocnicc  40669  etransclem14  40941  etransclem17  40944  etransclem21  40948  etransclem25  40952  etransclem28  40955  etransclem31  40958  hsphoif  41269  hoidmvval  41270  hsphoival  41272  hoidmvlelem5  41292  hoidmvle  41293  ovnhoi  41296  hspmbllem2  41320