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

Theorem ifeq1d 4053
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 4039 . 2 (𝐴 = 𝐵 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
31, 2syl 17 1 (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  ifcif 4035
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-rab 2904  df-v 3174  df-un 3544  df-if 4036
This theorem is referenced by:  ifeq12d  4055  ifbieq1d  4058  ifeq1da  4065  rabsnif  4201  fsuppmptif  8165  cantnflem1  8446  sumeq2w  14216  cbvsum  14219  isumless  14362  prodss  14462  subgmulg  17377  evlslem2  19279  dmatcrng  20069  scmatscmiddistr  20075  scmatcrng  20088  marrepfval  20127  mdetr0  20172  mdetunilem8  20186  madufval  20204  madugsum  20210  minmar1fval  20213  decpmatid  20336  monmatcollpw  20345  pmatcollpwscmatlem1  20355  cnmpt2pc  22466  pcoval2  22555  pcopt  22561  itgz  23270  iblss2  23295  itgss  23301  itgcn  23332  plyeq0lem  23687  dgrcolem2  23751  plydivlem4  23772  leibpi  24386  chtublem  24653  sumdchr  24714  bposlem6  24731  lgsval  24743  dchrvmasumiflem2  24908  padicabvcxp  25038  dfrdg3  30752  matunitlindflem1  32371  ftc1anclem2  32452  ftc1anclem5  32455  ftc1anclem7  32457  hoidifhspval  39295  hoimbl  39318
  Copyright terms: Public domain W3C validator