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

Theorem ifeq2d 3699
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 3689 . 2  |-  ( A  =  B  ->  if ( ps ,  C ,  A )  =  if ( ps ,  C ,  B ) )
31, 2syl 16 1  |-  ( ph  ->  if ( ps ,  C ,  A )  =  if ( ps ,  C ,  B )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649   ifcif 3684
This theorem is referenced by:  ifeq12d  3700  ifbieq2d  3704  ifeq2da  3710  rdgeq1  6607  cantnflem1d  7579  cantnflem1  7580  rexmul  10784  1arithlem4  13223  ramcl  13326  mplcoe1  16457  mplcoe2  16459  subrgascl  16487  itg2monolem1  19511  iblmulc2  19591  itgmulc2lem1  19592  bddmulibl  19599  dvtaylp  20155  dchrinvcl  20906  rpvmasum2  21075  padicfval  21179  gxval  21696  itgmulc2nclem1  25973  hdmap1fval  31914
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2370
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2376  df-cleq 2382  df-clel 2385  df-nfc 2514  df-rab 2660  df-v 2903  df-un 3270  df-if 3685
  Copyright terms: Public domain W3C validator