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

Theorem ifeq12d 3522
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 3520 . 2  |-  ( ph  ->  if ( ps ,  A ,  C )  =  if ( ps ,  B ,  C )
)
3 ifeq12d.2 . . 3  |-  ( ph  ->  C  =  D )
43ifeq2d 3521 . 2  |-  ( ph  ->  if ( ps ,  B ,  C )  =  if ( ps ,  B ,  D )
)
52, 4eqtrd 2288 1  |-  ( ph  ->  if ( ps ,  A ,  C )  =  if ( ps ,  B ,  D )
)
Colors of variables: wff set class
Syntax hints:    -> wi 6    = wceq 1619   ifcif 3506
This theorem is referenced by:  ifbieq12d  3528  oev  6446  dfac12r  7705  xaddpnf1  10484  ruclem1  12436  eucalgval  12679  gsumpropd  14380  gsumress  14381  mulgfval  14495  mulgpropd  14527  frgpup3lem  15013  subrgmvr  16132  isobs  16547  pcoval  18436  pcorevlem  18451  itg2const  19022  ditgeq3  19127  efrlim  20191  lgsval  20466  rpvmasum2  20588  gxfval  20849  gxval  20850  prodeq2  24639  isconc1  25338  isconc2  25339  isconc3  25340  uvcfval  26565  dgrsub2  26671  hdmap1fval  31117
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-rab 2523  df-v 2742  df-un 3099  df-if 3507
  Copyright terms: Public domain W3C validator