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

Theorem ifeq12d 3910
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 3908 . 2  |-  ( ph  ->  if ( ps ,  A ,  C )  =  if ( ps ,  B ,  C )
)
3 ifeq12d.2 . . 3  |-  ( ph  ->  C  =  D )
43ifeq2d 3909 . 2  |-  ( ph  ->  if ( ps ,  B ,  C )  =  if ( ps ,  B ,  D )
)
52, 4eqtrd 2492 1  |-  ( ph  ->  if ( ps ,  A ,  C )  =  if ( ps ,  B ,  D )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1370   ifcif 3892
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-rab 2804  df-v 3073  df-un 3434  df-if 3893
This theorem is referenced by:  ifbieq12d  3917  csbif  3940  oev  7057  dfac12r  8419  xaddpnf1  11300  swrdccat3blem  12497  ruclem1  13624  eucalgval  13868  gsumpropd  15615  gsumpropd2lem  15616  gsumress  15618  mulgfval  15739  mulgpropd  15771  frgpup3lem  16387  subrgmvr  17656  isobs  18263  uvcfval  18327  matsc  18461  marrepval0  18492  marepvval0  18497  mulmarep1el  18503  madufval  18568  madugsum  18574  minmar1fval  18577  pcoval  20708  pcorevlem  20723  itg2const  21344  ditgeq3  21451  efrlim  22489  lgsval  22765  rpvmasum2  22887  gxfval  23889  gxval  23890  xrhval  26582  itg2addnclem  28584  ftc1anclem5  28612  dgrsub2  29632  scmatel  31013  pmat1opsc  31168  pmat1ovscd  31169  mat2pmat1  31198  pmatcollpw1id  31229  idpmattoidmply1  31263  hdmap1fval  35751
  Copyright terms: Public domain W3C validator