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

Theorem ifeq12d 3959
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 3957 . 2  |-  ( ph  ->  if ( ps ,  A ,  C )  =  if ( ps ,  B ,  C )
)
3 ifeq12d.2 . . 3  |-  ( ph  ->  C  =  D )
43ifeq2d 3958 . 2  |-  ( ph  ->  if ( ps ,  B ,  C )  =  if ( ps ,  B ,  D )
)
52, 4eqtrd 2508 1  |-  ( ph  ->  if ( ps ,  A ,  C )  =  if ( ps ,  B ,  D )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1379   ifcif 3939
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rab 2823  df-v 3115  df-un 3481  df-if 3940
This theorem is referenced by:  ifbieq12d  3966  csbif  3989  oev  7161  dfac12r  8522  xaddpnf1  11421  swrdccat3blem  12679  ruclem1  13821  eucalgval  14066  gsumpropd  15817  gsumpropd2lem  15818  gsumress  15820  mulgfval  15943  mulgpropd  15975  frgpup3lem  16591  subrgmvr  17894  isobs  18518  uvcfval  18582  matsc  18719  scmatscmide  18776  marrepval0  18830  marepvval0  18835  mulmarep1el  18841  madufval  18906  madugsum  18912  minmar1fval  18915  pmat1opsc  18967  pmat1ovscd  18968  mat2pmat1  19000  decpmatid  19038  idpm2idmp  19069  pcoval  21246  pcorevlem  21261  itg2const  21882  ditgeq3  21989  efrlim  23027  lgsval  23303  rpvmasum2  23425  gxfval  24935  gxval  24936  xrhval  27632  itg2addnclem  29643  ftc1anclem5  29671  dgrsub2  30688  ifeq123d  31014  dirkerval  31391  fourierdlem111  31518  fourierdlem112  31519  fourierdlem113  31520  hdmap1fval  36594
  Copyright terms: Public domain W3C validator