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

Theorem ifeq12d 3583
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 3581 . 2  |-  ( ph  ->  if ( ps ,  A ,  C )  =  if ( ps ,  B ,  C )
)
3 ifeq12d.2 . . 3  |-  ( ph  ->  C  =  D )
43ifeq2d 3582 . 2  |-  ( ph  ->  if ( ps ,  B ,  C )  =  if ( ps ,  B ,  D )
)
52, 4eqtrd 2317 1  |-  ( ph  ->  if ( ps ,  A ,  C )  =  if ( ps ,  B ,  D )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1625   ifcif 3567
This theorem is referenced by:  ifbieq12d  3589  oev  6515  dfac12r  7774  xaddpnf1  10555  ruclem1  12511  eucalgval  12754  gsumpropd  14455  gsumress  14456  mulgfval  14570  mulgpropd  14602  frgpup3lem  15088  subrgmvr  16207  isobs  16622  pcoval  18511  pcorevlem  18526  itg2const  19097  ditgeq3  19202  efrlim  20266  lgsval  20541  rpvmasum2  20663  gxfval  20926  gxval  20927  gsumpropd2lem  23381  itg2addnclem  24933  prodeq2  25318  isconc1  26017  isconc2  26018  isconc3  26019  uvcfval  27244  dgrsub2  27350  hdmap1fval  32060
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-rab 2554  df-v 2792  df-un 3159  df-if 3568
  Copyright terms: Public domain W3C validator