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

Theorem ifeq1d 3957
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 3943 . 2 (𝐴 = 𝐵 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
31, 2syl 17 1 (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  ifcif 3939
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1699  df-sb 1831  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-rab 2809  df-v 3079  df-un 3449  df-if 3940
This theorem is referenced by:  ifeq12d  3959  ifbieq1d  3962  ifeq1da  3969  rabsnif  4105  fsuppmptif  8068  cantnflem1  8349  sumeq2w  14143  cbvsum  14146  isumless  14289  prodss  14389  subgmulg  17327  evlslem2  19241  dmatcrng  20034  scmatscmiddistr  20040  scmatcrng  20053  marrepfval  20092  mdetr0  20137  mdetunilem8  20151  madufval  20169  madugsum  20175  minmar1fval  20178  decpmatid  20301  monmatcollpw  20310  pmatcollpwscmatlem1  20320  cnmpt2pc  22462  pcoval2  22551  pcopt  22557  itgz  23232  iblss2  23257  itgss  23263  itgcn  23294  plyeq0lem  23658  dgrcolem2  23722  plydivlem4  23743  leibpi  24360  chtublem  24629  sumdchr  24690  bposlem6  24707  lgsval  24719  dchrvmasumiflem2  24884  padicabvcxp  25014  dfrdg3  30792  matunitlindflem1  32469  ftc1anclem2  32550  ftc1anclem5  32553  ftc1anclem7  32555  hoidifhspval  39409  hoimbl  39432
  Copyright terms: Public domain W3C validator