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

Theorem ifeq12d 3594
Description: Equality deduction for conditional operator. (Contributed by NM, 24-Mar-2015.)
Hypotheses
Ref Expression
ifeq1d.1  |-  ( ph  ->  A  =  B )
ifeq12d.2  |-  ( ph  ->  C  =  D )
Assertion
Ref Expression
ifeq12d  |-  ( ph  ->  if ( ps ,  A ,  C )  =  if ( ps ,  B ,  D )
)

Proof of Theorem ifeq12d
StepHypRef Expression
1 ifeq1d.1 . . 3  |-  ( ph  ->  A  =  B )
21ifeq1d 3592 . 2  |-  ( ph  ->  if ( ps ,  A ,  C )  =  if ( ps ,  B ,  C )
)
3 ifeq12d.2 . . 3  |-  ( ph  ->  C  =  D )
43ifeq2d 3593 . 2  |-  ( ph  ->  if ( ps ,  B ,  C )  =  if ( ps ,  B ,  D )
)
52, 4eqtrd 2328 1  |-  ( ph  ->  if ( ps ,  A ,  C )  =  if ( ps ,  B ,  D )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632   ifcif 3578
This theorem is referenced by:  ifbieq12d  3600  oev  6529  dfac12r  7788  xaddpnf1  10569  ruclem1  12525  eucalgval  12768  gsumpropd  14469  gsumress  14470  mulgfval  14584  mulgpropd  14616  frgpup3lem  15102  subrgmvr  16221  isobs  16636  pcoval  18525  pcorevlem  18540  itg2const  19111  ditgeq3  19216  efrlim  20280  lgsval  20555  rpvmasum2  20677  gxfval  20940  gxval  20941  gsumpropd2lem  23394  itg2addnclem  25003  prodeq2  25410  isconc1  26109  isconc2  26110  isconc3  26111  uvcfval  27336  dgrsub2  27442  hdmap1fval  32609
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rab 2565  df-v 2803  df-un 3170  df-if 3579
  Copyright terms: Public domain W3C validator