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

Theorem ifeq12d 3747
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 3745 . 2  |-  ( ph  ->  if ( ps ,  A ,  C )  =  if ( ps ,  B ,  C )
)
3 ifeq12d.2 . . 3  |-  ( ph  ->  C  =  D )
43ifeq2d 3746 . 2  |-  ( ph  ->  if ( ps ,  B ,  C )  =  if ( ps ,  B ,  D )
)
52, 4eqtrd 2467 1  |-  ( ph  ->  if ( ps ,  A ,  C )  =  if ( ps ,  B ,  D )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652   ifcif 3731
This theorem is referenced by:  ifbieq12d  3753  oev  6750  dfac12r  8018  xaddpnf1  10804  ruclem1  12822  eucalgval  13065  gsumpropd  14768  gsumress  14769  mulgfval  14883  mulgpropd  14915  frgpup3lem  15401  subrgmvr  16516  isobs  16939  pcoval  19028  pcorevlem  19043  itg2const  19624  ditgeq3  19729  efrlim  20800  lgsval  21076  rpvmasum2  21198  gxfval  21837  gxval  21838  gsumpropd2lem  24212  xrhval  24376  itg2addnclem  26246  uvcfval  27191  dgrsub2  27297  swrdccat3blem  28174  hdmap1fval  32522
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-rab 2706  df-v 2950  df-un 3317  df-if 3732
  Copyright terms: Public domain W3C validator