Theorem ifeq1d 4076

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

Syntax hints:   → wi 4   = wceq 1480  ifcif 4058

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-rab 2916  df-v 3188  df-un 3560  df-if 4059

This theorem is referenced by:  ifeq12d  4078  ifbieq1d  4081  ifeq1da  4088  rabsnif  4228  fsuppmptif  8249  cantnflem1  8530  sumeq2w  14356  cbvsum  14359  isumless  14502  prodss  14602  subgmulg  17529  evlslem2  19431  dmatcrng  20227  scmatscmiddistr  20233  scmatcrng  20246  marrepfval  20285  mdetr0  20330  mdetunilem8  20344  madufval  20362  madugsum  20368  minmar1fval  20371  decpmatid  20494  monmatcollpw  20503  pmatcollpwscmatlem1  20513  cnmpt2pc  22635  pcoval2  22724  pcopt  22730  itgz  23453  iblss2  23478  itgss  23484  itgcn  23515  plyeq0lem  23870  dgrcolem2  23934  plydivlem4  23955  leibpi  24569  chtublem  24836  sumdchr  24897  bposlem6  24914  lgsval  24926  dchrvmasumiflem2  25091  padicabvcxp  25221  dfrdg3  31400  matunitlindflem1  33034  ftc1anclem2  33115  ftc1anclem5  33118  ftc1anclem7  33120  hoidifhspval  40126  hoimbl  40149