Theorem ifeq1d 3926

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

Syntax hints:   → wi 4   = wceq 1468  ifcif 3908

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1698  ax-4 1711  ax-5 1789  ax-6 1836  ax-7 1883  ax-10 1965  ax-11 1970  ax-12 1983  ax-13 2137  ax-ext 2485

This theorem depends on definitions:  df-bi 192  df-or 379  df-an 380  df-tru 1471  df-ex 1693  df-nf 1697  df-sb 1829  df-clab 2492  df-cleq 2498  df-clel 2501  df-nfc 2635  df-rab 2800  df-v 3068  df-un 3431  df-if 3909

This theorem is referenced by:  ifeq12d  3928  ifbieq1d  3931  ifeq1da  3938  rabsnif  4069  fsuppmptif  7998  cantnflem1  8279  sumeq2w  13918  cbvsum  13921  isumless  14063  prodss  14161  subgmulg  16991  evlslem2  18894  dmatcrng  19685  scmatscmiddistr  19691  scmatcrng  19704  marrepfval  19743  mdetr0  19788  mdetunilem8  19802  madufval  19820  madugsum  19826  minmar1fval  19829  decpmatid  19952  monmatcollpw  19961  pmatcollpwscmatlem1  19971  cnmpt2pc  22114  pcoval2  22206  pcopt  22212  itgz  22899  iblss2  22924  itgss  22930  itgcn  22961  plyeq0lem  23325  dgrcolem2  23389  plydivlem4  23410  leibpi  24029  chtublem  24300  sumdchr  24361  bposlem6  24378  lgsval  24389  dchrvmasumiflem2  24501  padicabvcxp  24631  dfrdg3  30594  matunitlindflem1  32174  ftc1anclem2  32256  ftc1anclem5  32259  ftc1anclem7  32261  hoidifhspval  38893  hoimbl  38916