Theorem ifeq1d 4502

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 4486	. 2 ⊢ (𝐴 = 𝐵 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
3	1, 2	syl 18	1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ifcif 4482

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-un 3904  df-if 4483

This theorem is used by:  ifeq12d  4504  ifbieq1d  4507  ifeq1da  4514  rabsnif  4684  fsuppmptif  9369  cantnflem1  9668  sumeq2w  15779  cbvsum  15782  cbvsumv  15783  sumeq2sdv  15790  isumless  15934  prodeq2sdv  16011  prodss  16034  subgmulg  19264  evlslem2  22295  selvval  22336  dmatcrng  22724  scmatscmiddistr  22730  scmatcrng  22743  marrepfval  22782  mdetr0  22827  mdetunilem8  22841  madufval  22859  madugsum  22865  minmar1fval  22868  matunitlindflem1  22901  decpmatid  22995  monmatcollpw  23004  pmatcollpwscmatlem1  23014  cnmpopc  25156  pcoval2  25244  pcopt  25250  itgz  26008  iblss2  26033  itgss  26039  itgcn  26072  plyeq0lem  26436  dgrcolem2  26500  plydivlem4  26526  leibpi  27179  chtublem  27447  sumdchr  27508  bposlem6  27525  lgsval  27537  dchrvmasumiflem2  27738  padicabvcxp  27868  mplasclco  34026  extvfv  34043  dfrdg3  36373  cbvsumdavw  36899  ftc1anclem2  38443  ftc1anclem5  38446  ftc1anclem7  38448  fsuppssindlem2  43438  fsuppssind  43439  mnringmulrvald  45065  hoidifhspval  47436  hoimbl  47459  veronesevald  50804