Theorem ifeq1d 4567

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

Syntax hints:   → wi 4   = wceq 1537  ifcif 4548

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-un 3981  df-if 4549

This theorem is referenced by:  ifeq12d  4569  ifbieq1d  4572  ifeq1da  4579  rabsnif  4748  fsuppmptif  9468  cantnflem1  9758  sumeq2w  15740  cbvsum  15743  cbvsumv  15744  sumeq2sdv  15751  isumless  15893  prodeq2sdv  15971  prodss  15995  subgmulg  19180  evlslem2  22126  selvval  22162  dmatcrng  22529  scmatscmiddistr  22535  scmatcrng  22548  marrepfval  22587  mdetr0  22632  mdetunilem8  22646  madufval  22664  madugsum  22670  minmar1fval  22673  decpmatid  22797  monmatcollpw  22806  pmatcollpwscmatlem1  22816  cnmpopc  24974  pcoval2  25068  pcopt  25074  itgz  25836  iblss2  25861  itgss  25867  itgcn  25900  plyeq0lem  26269  dgrcolem2  26334  plydivlem4  26356  leibpi  27003  chtublem  27273  sumdchr  27334  bposlem6  27351  lgsval  27363  dchrvmasumiflem2  27564  padicabvcxp  27694  dfrdg3  35760  cbvsumdavw  36245  matunitlindflem1  37576  ftc1anclem2  37654  ftc1anclem5  37657  ftc1anclem7  37659  fsuppssindlem2  42547  fsuppssind  42548  mnringmulrvald  44196  hoidifhspval  46529  hoimbl  46552