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

Theorem ifeq2d 3903
Description: Equality deduction for conditional operator. (Contributed by NM, 16-Feb-2005.)
Hypothesis
Ref Expression
ifeq1d.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
ifeq2d  |-  ( ph  ->  if ( ps ,  C ,  A )  =  if ( ps ,  C ,  B )
)

Proof of Theorem ifeq2d
StepHypRef Expression
1 ifeq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 ifeq2 3889 . 2  |-  ( A  =  B  ->  if ( ps ,  C ,  A )  =  if ( ps ,  C ,  B ) )
31, 2syl 17 1  |-  ( ph  ->  if ( ps ,  C ,  A )  =  if ( ps ,  C ,  B )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1405   ifcif 3884
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-rab 2762  df-v 3060  df-un 3418  df-if 3885
This theorem is referenced by:  ifeq12d  3904  ifbieq2d  3909  ifeq2da  3915  ifcomnan  3933  rdgeq1  7113  cantnflem1d  8138  cantnflem1  8139  cantnflem1dOLD  8161  cantnflem1OLD  8162  rexmul  11515  1arithlem4  14651  ramcl  14754  mplcoe1  18445  mplcoe5  18449  mplcoe2OLD  18451  subrgascl  18481  scmatscm  19305  marrepfval  19352  ma1repveval  19363  mulmarep1el  19364  mdetralt2  19401  mdetunilem8  19411  maduval  19430  maducoeval2  19432  madurid  19436  minmar1val0  19439  monmatcollpw  19570  pmatcollpwscmatlem1  19580  monmat2matmon  19615  itg2monolem1  22447  iblmulc2  22527  itgmulc2lem1  22528  bddmulibl  22535  dvtaylp  23055  dchrinvcl  23907  rpvmasum2  24076  padicfval  24180  gxval  25660  plymulx  28997  itg2addnclem  31419  itg2addnclem3  31421  itg2addnc  31422  itgmulc2nclem1  31434  hdmap1fval  34797  itgioocnicc  37125  etransclem14  37380  etransclem17  37383  etransclem21  37387  etransclem25  37391  etransclem28  37394  etransclem31  37397
  Copyright terms: Public domain W3C validator