Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ifeq1d Structured version   Visualization version   GIF version

Theorem ifeq1d 4442
 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
StepHypRef Expression
1 ifeq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 ifeq1 4427 . 2 (𝐴 = 𝐵 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
31, 2syl 17 1 (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1538  ifcif 4423 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-12 2175  ax-ext 2729 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-rab 3079  df-v 3411  df-un 3865  df-if 4424 This theorem is referenced by:  ifeq12d  4444  ifbieq1d  4447  ifeq1da  4454  rabsnif  4619  fsuppmptif  8909  cantnflem1  9198  sumeq2w  15110  cbvsum  15113  isumless  15261  prodss  15362  subgmulg  18374  evlslem2  20856  selvval  20895  dmatcrng  21216  scmatscmiddistr  21222  scmatcrng  21235  marrepfval  21274  mdetr0  21319  mdetunilem8  21333  madufval  21351  madugsum  21357  minmar1fval  21360  decpmatid  21484  monmatcollpw  21493  pmatcollpwscmatlem1  21503  cnmpopc  23643  pcoval2  23731  pcopt  23737  itgz  24494  iblss2  24519  itgss  24525  itgcn  24558  plyeq0lem  24920  dgrcolem2  24984  plydivlem4  25005  leibpi  25641  chtublem  25908  sumdchr  25969  bposlem6  25986  lgsval  25998  dchrvmasumiflem2  26199  padicabvcxp  26329  dfrdg3  33301  matunitlindflem1  35368  ftc1anclem2  35446  ftc1anclem5  35449  ftc1anclem7  35451  fsuppssindlem2  39825  fsuppssind  39826  mnringmulrvald  41353  hoidifhspval  43658  hoimbl  43681
 Copyright terms: Public domain W3C validator