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

Theorem ifbieq12d 3761
Description: Equivalence deduction for conditional operators. (Contributed by Jeff Madsen, 2-Sep-2009.)
Hypotheses
Ref Expression
ifbieq12d.1  |-  ( ph  ->  ( ps  <->  ch )
)
ifbieq12d.2  |-  ( ph  ->  A  =  C )
ifbieq12d.3  |-  ( ph  ->  B  =  D )
Assertion
Ref Expression
ifbieq12d  |-  ( ph  ->  if ( ps ,  A ,  B )  =  if ( ch ,  C ,  D )
)

Proof of Theorem ifbieq12d
StepHypRef Expression
1 ifbieq12d.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21ifbid 3757 . 2  |-  ( ph  ->  if ( ps ,  A ,  B )  =  if ( ch ,  A ,  B )
)
3 ifbieq12d.2 . . 3  |-  ( ph  ->  A  =  C )
4 ifbieq12d.3 . . 3  |-  ( ph  ->  B  =  D )
53, 4ifeq12d 3755 . 2  |-  ( ph  ->  if ( ch ,  A ,  B )  =  if ( ch ,  C ,  D )
)
62, 5eqtrd 2468 1  |-  ( ph  ->  if ( ps ,  A ,  B )  =  if ( ch ,  C ,  D )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1652   ifcif 3739
This theorem is referenced by:  csbifg  3767  opeq1  3984  opeq2  3985  riotaeqdv  6550  riotabidv  6551  tz7.44-2  6665  tz7.44-3  6666  boxcutc  7105  unxpdomlem1  7313  oieq1  7481  oieq2  7482  cantnflem1d  7644  cantnflem1  7645  iunfictbso  7995  dfac12lem1  8023  dfac12r  8026  fin23lem12  8211  fin23lem33  8225  ttukeylem3  8391  ttukey2g  8396  xaddval  10809  seqf1olem2  11363  expval  11384  bcval  11595  ccatfval  11742  ccatval1  11745  ccatval2  11746  swrdval  11764  cbvsum  12489  summolem2a  12509  zsum  12512  fsum  12514  sumss  12518  sumss2  12520  fsumcvg2  12521  fsumser  12524  isumless  12625  rpnnen2lem1  12814  rpnnen  12826  ruclem1  12830  sadadd2lem  12971  sadadd2  12972  eucalgval2  13072  pcmpt  13261  pcmptdvds  13263  prmreclem2  13285  prmreclem4  13287  prmreclem5  13288  prmreclem6  13289  prmrec  13290  ramub1lem2  13395  ramcl  13397  ressval  13516  gsumvalx  14774  gsumpropd  14776  gsumress  14777  mulgval  14892  cyggenod2  15495  dmdprdsplitlem  15595  mvrfval  16484  evlslem2  16568  coe1tmmul2fv  16670  coe1pwmulfv  16672  xrsdsval  16742  cyggic  16853  fclsval  18040  ptcmplem3  18085  stdbdmetval  18544  stdbdxmet  18545  xrhmeo  18971  phtpycc  19016  pcovalg  19037  pcocn  19042  pcohtpylem  19044  pcopt2  19048  pcoass  19049  pcorevlem  19051  cmetcaulem  19241  ovolunlem1a  19392  ovolunlem1  19393  ovolicc2lem3  19415  ovolicc2lem4  19416  ovolicc2lem5  19417  ioombl1  19456  mbfmax  19541  mbfpos  19543  mbfposb  19545  i1fres  19597  i1fposd  19599  mbfi1fseqlem2  19608  mbfi1fseq  19613  mbfi1flimlem  19614  mbfi1flim  19615  itg2splitlem  19640  itg2cnlem1  19653  itg2cn  19655  isibl  19657  isibl2  19658  iblitg  19660  dfitg  19661  cbvitg  19667  itgeq2  19669  itgvallem  19676  iblneg  19694  itgneg  19695  itgss3  19706  itgcn  19734  ditgeq1  19735  ditgeq2  19736  deg1suble  20030  ig1pval  20095  elply2  20115  dgrsub  20190  aareccl  20243  cxpval  20555  vmaval  20896  prmorcht  20961  musumsum  20977  muinv  20978  pclogsum  20999  dchrelbasd  21023  dchrptlem2  21049  bposlem5  21072  lgsval  21084  lgsfval  21085  lgsdir  21114  lgsdilem2  21115  lgsdi  21116  lgsne0  21117  rplogsumlem2  21179  pntrlog2bndlem4  21274  pntrlog2bndlem5  21275  gxval  21846  gsumpropd2lem  24220  ballotlemsval  24766  ballotlemsv  24767  ballotlemsf1o  24771  ballotlemieq  24774  lgamgulmlem4  24816  lgamgulmlem5  24817  cbvprod  25241  prodmolem2a  25260  zprod  25263  fprod  25267  fprodntriv  25268  prodss  25273  rdgprc0  25421  dfrdg2  25423  mblfinlem2  26244  itg2addnclem  26256  itg2addnclem3  26258  itgaddnclem2  26264  ftc1anclem5  26284  ftc1anclem6  26285  aomclem8  27136  pmtrval  27371  pmtrfv  27372  afveq12d  27973  cdleme27b  31165  cdleme29b  31172  cdleme31sn  31177  cdleme31fv  31187  cdleme40v  31266  cdlemk40  31714  dihffval  32028  dihfval  32029  dihval  32030
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-rab 2714  df-v 2958  df-un 3325  df-if 3740
  Copyright terms: Public domain W3C validator