Theorem ifeq1d 4487

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

Syntax hints:   → wi 4   = wceq 1537  ifcif 4469

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-rab 3149  df-v 3498  df-un 3943  df-if 4470

This theorem is referenced by:  ifeq12d  4489  ifbieq1d  4492  ifeq1da  4499  rabsnif  4661  fsuppmptif  8865  cantnflem1  9154  sumeq2w  15051  cbvsum  15054  isumless  15202  prodss  15303  subgmulg  18295  evlslem2  20294  selvval  20333  dmatcrng  21113  scmatscmiddistr  21119  scmatcrng  21132  marrepfval  21171  mdetr0  21216  mdetunilem8  21230  madufval  21248  madugsum  21254  minmar1fval  21257  decpmatid  21380  monmatcollpw  21389  pmatcollpwscmatlem1  21399  cnmpopc  23534  pcoval2  23622  pcopt  23628  itgz  24383  iblss2  24408  itgss  24414  itgcn  24445  plyeq0lem  24802  dgrcolem2  24866  plydivlem4  24887  leibpi  25522  chtublem  25789  sumdchr  25850  bposlem6  25867  lgsval  25879  dchrvmasumiflem2  26080  padicabvcxp  26210  dfrdg3  33043  matunitlindflem1  34890  ftc1anclem2  34970  ftc1anclem5  34973  ftc1anclem7  34975  hoidifhspval  42897  hoimbl  42920