Theorem ifeq1d 4240

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

Syntax hints:   → wi 4   = wceq 1624  ifcif 4222

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-rab 3051  df-v 3334  df-un 3712  df-if 4223

This theorem is referenced by:  ifeq12d  4242  ifbieq1d  4245  ifeq1da  4252  rabsnif  4394  fsuppmptif  8462  cantnflem1  8751  sumeq2w  14613  cbvsum  14616  isumless  14768  prodss  14868  subgmulg  17801  evlslem2  19706  dmatcrng  20502  scmatscmiddistr  20508  scmatcrng  20521  marrepfval  20560  mdetr0  20605  mdetunilem8  20619  madufval  20637  madugsum  20643  minmar1fval  20646  decpmatid  20769  monmatcollpw  20778  pmatcollpwscmatlem1  20788  cnmpt2pc  22920  pcoval2  23008  pcopt  23014  itgz  23738  iblss2  23763  itgss  23769  itgcn  23800  plyeq0lem  24157  dgrcolem2  24221  plydivlem4  24242  leibpi  24860  chtublem  25127  sumdchr  25188  bposlem6  25205  lgsval  25217  dchrvmasumiflem2  25382  padicabvcxp  25512  dfrdg3  31999  matunitlindflem1  33710  ftc1anclem2  33791  ftc1anclem5  33794  ftc1anclem7  33796  hoidifhspval  41320  hoimbl  41343