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

Theorem ifeq12d 3935
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 3933 . 2  |-  ( ph  ->  if ( ps ,  A ,  C )  =  if ( ps ,  B ,  C )
)
3 ifeq12d.2 . . 3  |-  ( ph  ->  C  =  D )
43ifeq2d 3934 . 2  |-  ( ph  ->  if ( ps ,  B ,  C )  =  if ( ps ,  B ,  D )
)
52, 4eqtrd 2470 1  |-  ( ph  ->  if ( ps ,  A ,  C )  =  if ( ps ,  B ,  D )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437   ifcif 3915
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-rab 2791  df-v 3089  df-un 3447  df-if 3916
This theorem is referenced by:  ifbieq12d  3942  csbif  3965  oev  7224  dfac12r  8574  xaddpnf1  11519  swrdccat3blem  12836  relexpsucnnr  13067  ruclem1  14261  eucalgval  14512  gsumpropd  16457  gsumpropd2lem  16458  gsumress  16461  mulgfval  16701  mulgpropd  16733  frgpup3lem  17353  subrgmvr  18611  isobs  19205  uvcfval  19264  matsc  19397  scmatscmide  19454  marrepval0  19508  marepvval0  19513  mulmarep1el  19519  madufval  19584  madugsum  19590  minmar1fval  19593  pmat1opsc  19645  pmat1ovscd  19646  mat2pmat1  19678  decpmatid  19716  idpm2idmp  19747  pcoval  21926  pcorevlem  21941  itg2const  22566  ditgeq3  22673  efrlim  23751  lgsval  24082  rpvmasum2  24204  gxfval  25821  gxval  25822  fzto1st  28446  psgnfzto1st  28448  xrhval  28652  itg2addnclem  31687  ftc1anclem5  31715  hdmap1fval  35064  dgrsub2  35690  dirkerval  37512  fourierdlem111  37639  fourierdlem112  37640  fourierdlem113  37641
  Copyright terms: Public domain W3C validator