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

Theorem ifeq12d 3804
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 3802 . 2  |-  ( ph  ->  if ( ps ,  A ,  C )  =  if ( ps ,  B ,  C )
)
3 ifeq12d.2 . . 3  |-  ( ph  ->  C  =  D )
43ifeq2d 3803 . 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 1369   ifcif 3786
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rab 2719  df-v 2969  df-un 3328  df-if 3787
This theorem is referenced by:  ifbieq12d  3811  csbif  3834  oev  6946  dfac12r  8307  xaddpnf1  11188  swrdccat3blem  12378  ruclem1  13505  eucalgval  13749  gsumpropd  15495  gsumpropd2lem  15496  gsumress  15498  mulgfval  15619  mulgpropd  15651  frgpup3lem  16265  subrgmvr  17517  isobs  18120  uvcfval  18184  matsc  18316  marrepval0  18347  marepvval0  18352  mulmarep1el  18358  madufval  18418  madugsum  18424  minmar1fval  18427  pcoval  20558  pcorevlem  20573  itg2const  21193  ditgeq3  21300  efrlim  22338  lgsval  22614  rpvmasum2  22736  gxfval  23695  gxval  23696  xrhval  26396  itg2addnclem  28396  ftc1anclem5  28424  dgrsub2  29444  hdmap1fval  35282
  Copyright terms: Public domain W3C validator