Theorem ifeq1d 4508

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

Syntax hints:   → wi 4   = wceq 1540  ifcif 4488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-un 3919  df-if 4489

This theorem is referenced by:  ifeq12d  4510  ifbieq1d  4513  ifeq1da  4520  rabsnif  4687  fsuppmptif  9350  cantnflem1  9642  sumeq2w  15658  cbvsum  15661  cbvsumv  15662  sumeq2sdv  15669  isumless  15811  prodeq2sdv  15889  prodss  15913  subgmulg  19072  evlslem2  21986  selvval  22022  dmatcrng  22389  scmatscmiddistr  22395  scmatcrng  22408  marrepfval  22447  mdetr0  22492  mdetunilem8  22506  madufval  22524  madugsum  22530  minmar1fval  22533  decpmatid  22657  monmatcollpw  22666  pmatcollpwscmatlem1  22676  cnmpopc  24822  pcoval2  24916  pcopt  24922  itgz  25682  iblss2  25707  itgss  25713  itgcn  25746  plyeq0lem  26115  dgrcolem2  26180  plydivlem4  26204  leibpi  26852  chtublem  27122  sumdchr  27183  bposlem6  27200  lgsval  27212  dchrvmasumiflem2  27413  padicabvcxp  27543  dfrdg3  35784  cbvsumdavw  36267  matunitlindflem1  37610  ftc1anclem2  37688  ftc1anclem5  37691  ftc1anclem7  37693  fsuppssindlem2  42580  fsuppssind  42581  mnringmulrvald  44216  hoidifhspval  46606  hoimbl  46629