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

Theorem ifbieq12d 3925
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 3920 . 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 3918 . 2  |-  ( ph  ->  if ( ch ,  A ,  B )  =  if ( ch ,  C ,  D )
)
62, 5eqtrd 2495 1  |-  ( ph  ->  if ( ps ,  A ,  B )  =  if ( ch ,  C ,  D )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1370   ifcif 3900
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 1955  ax-ext 2432
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 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-rab 2808  df-v 3080  df-un 3442  df-if 3901
This theorem is referenced by:  csbif  3948  csbifgOLD  3949  tz7.44-2  6974  tz7.44-3  6975  boxcutc  7417  unxpdomlem1  7629  dfac12lem1  8424  dfac12r  8427  fin23lem12  8612  fin23lem33  8626  ttukeylem3  8792  ttukey2g  8797  xaddval  11305  seqf1olem2  11964  expval  11985  ccatfval  12392  ccatval1  12395  ccatval2  12396  ruclem1  13632  eucalgval2  13875  ressval  14345  gsumvalx  15622  gsumpropd  15624  gsumpropd2lem  15625  gsumress  15627  mulgval  15749  pmtrval  16077  pmtrfv  16078  mvrfval  17618  xrsdsval  17983  marrepeval  18502  marepveval  18507  mdetunilem9  18559  maducoeval  18578  maducoeval2  18579  madutpos  18581  madugsum  18582  minmar1eval  18588  symgmatr01lem  18592  symgmatr01  18593  gsummatr01lem3  18596  gsummatr01lem4  18597  gsummatr01  18598  ptcmplem3  19759  xrhmeo  20651  phtpycc  20696  pcovalg  20717  pcocn  20722  pcohtpylem  20724  pcoass  20729  pcorevlem  20731  ovolunlem1a  21112  ovolunlem1  21113  ioombl1  21177  mbfmax  21261  mbfpos  21263  mbfi1fseqlem2  21328  mbfi1fseq  21333  ditgeq1  21457  ditgeq2  21458  ig1pval  21778  cxpval  22243  musumsum  22666  muinv  22667  lgsval  22773  gxval  23898  resvval  26441  ballotlemsval  27036  ballotlemsv  27037  ballotlemsf1o  27041  ballotlemieq  27044  plymulx0  27093  lgamgulmlem4  27163  lgamgulmlem5  27164  cbvprod  27573  prodmolem2a  27592  zprod  27595  fprod  27599  fprodntriv  27600  prodss  27605  rdgprc0  27752  dfrdg2  27754  mblfinlem2  28578  itg2addnclem3  28594  itgaddnclem2  28600  ftc1anclem5  28620  ftc1anclem6  28621  aomclem8  29563  afveq12d  30188  clwlkisclwwlklem2fv1  30593  fvmptnn04if  31336  cdleme27b  34351  cdleme29b  34358  cdleme31sn  34363  cdleme31fv  34373  cdleme40v  34452  cdlemk40  34900  dihffval  35214  dihfval  35215  dihval  35216
  Copyright terms: Public domain W3C validator