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

Theorem ifeq1d 4487
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 4473 . 2 (𝐴 = 𝐵 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
31, 2syl 17 1 (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1530  ifcif 4469
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2152  ax-12 2167  ax-ext 2796
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2803  df-cleq 2817  df-clel 2897  df-nfc 2967  df-rab 3151  df-v 3501  df-un 3944  df-if 4470
This theorem is referenced by:  ifeq12d  4489  ifbieq1d  4492  ifeq1da  4499  rabsnif  4657  fsuppmptif  8855  cantnflem1  9144  sumeq2w  15041  cbvsum  15044  isumless  15192  prodss  15293  subgmulg  18225  evlslem2  20212  selvval  20248  dmatcrng  21027  scmatscmiddistr  21033  scmatcrng  21046  marrepfval  21085  mdetr0  21130  mdetunilem8  21144  madufval  21162  madugsum  21168  minmar1fval  21171  decpmatid  21294  monmatcollpw  21303  pmatcollpwscmatlem1  21313  cnmpopc  23447  pcoval2  23535  pcopt  23541  itgz  24296  iblss2  24321  itgss  24327  itgcn  24358  plyeq0lem  24715  dgrcolem2  24779  plydivlem4  24800  leibpi  25434  chtublem  25701  sumdchr  25762  bposlem6  25779  lgsval  25791  dchrvmasumiflem2  25992  padicabvcxp  26122  dfrdg3  32926  matunitlindflem1  34756  ftc1anclem2  34836  ftc1anclem5  34839  ftc1anclem7  34841  hoidifhspval  42753  hoimbl  42776
  Copyright terms: Public domain W3C validator