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

Theorem ifeq2d 4488
Description: Equality deduction for conditional operator. (Contributed by NM, 16-Feb-2005.)
Hypothesis
Ref Expression
ifeq1d.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
ifeq2d (𝜑 → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵))

Proof of Theorem ifeq2d
StepHypRef Expression
1 ifeq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 ifeq2 4474 . 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 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797
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 2804  df-cleq 2818  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  ifbieq2d  4494  ifeq2da  4500  ifcomnan  4523  rdgeq1  8041  cantnflem1d  9143  cantnflem1  9144  rexmul  12657  1arithlem4  16254  ramcl  16357  mplcoe1  20166  mplcoe5  20169  subrgascl  20198  selvffval  20248  selvval  20250  scmatscm  21040  marrepfval  21087  ma1repveval  21098  mulmarep1el  21099  mdetralt2  21136  mdetunilem8  21146  maduval  21165  maducoeval2  21167  madurid  21171  minmar1val0  21174  monmatcollpw  21305  pmatcollpwscmatlem1  21315  monmat2matmon  21350  itg2monolem1  24268  iblmulc2  24348  itgmulc2lem1  24349  bddmulibl  24356  dvtaylp  24875  dchrinvcl  25745  rpvmasum2  26004  padicfval  26108  plymulx  31706  itg2addnclem  34812  itg2addnclem3  34814  itg2addnc  34815  itgmulc2nclem1  34827  hdmap1fval  38801  itgioocnicc  42129  etransclem14  42401  etransclem17  42404  etransclem21  42408  etransclem25  42412  etransclem28  42415  etransclem31  42418  hsphoif  42726  hoidmvval  42727  hsphoival  42729  hoidmvlelem5  42749  hoidmvle  42750  ovnhoi  42753  hspmbllem2  42777
  Copyright terms: Public domain W3C validator