Theorem ifeq1d 4501

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

Hypothesis

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

Assertion

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

Proof of Theorem ifeq1d

Step	Hyp	Ref	Expression
1		ifeq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		ifeq1 4485	. 2 ⊢ (𝐴 = 𝐵 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
3	1, 2	syl 18	1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))

This proof depends on syntax axioms:   → wi 4   = wceq 1569  ifcif 4481

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-un 4151  df-if 4482

This theorem is used by:  ifeq12d  4503  ifbieq1d  4506  ifeq1da  4513  rabsnif  4680  fsuppmptif  9395  cantnflem1  9694  sumeq2w  15865  cbvsum  15868  cbvsumv  15869  sumeq2sdv  15876  isumless  16020  prodeq2sdv  16097  prodss  16120  subgmulg  19357  evlslem2  22394  selvval  22435  dmatcrng  22823  scmatscmiddistr  22829  scmatcrng  22842  marrepfval  22881  mdetr0  22926  mdetunilem8  22940  madufval  22958  madugsum  22964  minmar1fval  22967  matunitlindflem1  23000  decpmatid  23094  monmatcollpw  23103  pmatcollpwscmatlem1  23113  cnmpopc  25255  pcoval2  25343  pcopt  25349  itgz  26107  iblss2  26132  itgss  26138  itgcn  26171  plyeq0lem  26535  dgrcolem2  26599  plydivlem4  26623  leibpi  27276  chtublem  27544  sumdchr  27605  bposlem6  27622  lgsval  27634  dchrvmasumiflem2  27835  padicabvcxp  27965  mplasclco  34195  extvfv  34212  dfrdg3  36651  cbvsumdavw  37161  ftc1anclem2  38706  ftc1anclem5  38709  ftc1anclem7  38711  fsuppssindlem2  43714  fsuppssind  43715  mnringmulrvald  45319  hoidifhspval  47712  hoimbl  47735  veronesevald  51140