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

Theorem ifeq2d 3580
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 3570 . 2  |-  ( A  =  B  ->  if ( ps ,  C ,  A )  =  if ( ps ,  C ,  B ) )
31, 2syl 15 1  |-  ( ph  ->  if ( ps ,  C ,  A )  =  if ( ps ,  C ,  B )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623   ifcif 3565
This theorem is referenced by:  ifeq12d  3581  ifbieq2d  3585  ifeq2da  3591  rdgeq1  6424  cantnflem1d  7390  cantnflem1  7391  rexmul  10591  1arithlem4  12973  ramcl  13076  mplcoe1  16209  mplcoe2  16211  subrgascl  16239  itg2monolem1  19105  iblmulc2  19185  itgmulc2lem1  19186  bddmulibl  19193  dvtaylp  19749  dchrinvcl  20492  rpvmasum2  20661  padicfval  20765  gxval  20925  prodeq3ii  25308  hdmap1fval  31987
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552  df-v 2790  df-un 3157  df-if 3566
  Copyright terms: Public domain W3C validator