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

Theorem ifeq12d 3555
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 3553 . 2  |-  ( ph  ->  if ( ps ,  A ,  C )  =  if ( ps ,  B ,  C )
)
3 ifeq12d.2 . . 3  |-  ( ph  ->  C  =  D )
43ifeq2d 3554 . 2  |-  ( ph  ->  if ( ps ,  B ,  C )  =  if ( ps ,  B ,  D )
)
52, 4eqtrd 2290 1  |-  ( ph  ->  if ( ps ,  A ,  C )  =  if ( ps ,  B ,  D )
)
Colors of variables: wff set class
Syntax hints:    -> wi 6    = wceq 1619   ifcif 3539
This theorem is referenced by:  ifbieq12d  3561  oev  6481  dfac12r  7740  xaddpnf1  10520  ruclem1  12472  eucalgval  12715  gsumpropd  14416  gsumress  14417  mulgfval  14531  mulgpropd  14563  frgpup3lem  15049  subrgmvr  16168  isobs  16583  pcoval  18472  pcorevlem  18487  itg2const  19058  ditgeq3  19163  efrlim  20227  lgsval  20502  rpvmasum2  20624  gxfval  20885  gxval  20886  prodeq2  24675  isconc1  25374  isconc2  25375  isconc3  25376  uvcfval  26601  dgrsub2  26707  hdmap1fval  31237
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 2239
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 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-rab 2527  df-v 2765  df-un 3132  df-if 3540
  Copyright terms: Public domain W3C validator