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

Theorem mp2and 661
Description: A deduction based on modus ponens. (Contributed by NM, 12-Dec-2004.)
Hypotheses
Ref Expression
mp2and.1  |-  ( ph  ->  ps )
mp2and.2  |-  ( ph  ->  ch )
mp2and.3  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
Assertion
Ref Expression
mp2and  |-  ( ph  ->  th )

Proof of Theorem mp2and
StepHypRef Expression
1 mp2and.2 . 2  |-  ( ph  ->  ch )
2 mp2and.1 . . 3  |-  ( ph  ->  ps )
3 mp2and.3 . . 3  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
42, 3mpand 657 . 2  |-  ( ph  ->  ( ch  ->  th )
)
51, 4mpd 15 1  |-  ( ph  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  ssnelpssd  3652  tfisi  4797  tfindsg2  4800  riotasv2d  6553  smoord  6586  oelimcl  6802  oeeui  6804  nnawordex  6839  omabs  6849  ertrd  6880  th3qlem1  6969  omxpenlem  7168  ixpfi2  7363  supmax  7426  oismo  7465  cantnflem1c  7599  cantnflem1  7601  cantnflem3  7603  infxpenc2  7859  axdc2lem  8284  r1limwun  8567  letrd  9183  lelttrd  9184  ltletrd  9186  lttrd  9187  le2addd  9600  le2subd  9601  ltleaddd  9602  leltaddd  9603  lt2subd  9605  ltmul12a  9822  lemul12ad  9909  lemul12bd  9910  lt2halvesd  10171  uzind  10317  uztrn  10458  xrlttrd  10705  xrlelttrd  10706  xrltletrd  10707  xrletrd  10708  supxrunb1  10854  supxrunb2  10855  ixxun  10888  ixxss1  10890  ixxss2  10891  ixxss12  10892  seqf1o  11319  faclbnd3  11538  sqrlem1  12003  sqrlem4  12006  sqrlem7  12009  abs3lemd  12218  rlimcn2  12339  o1of2  12361  lo1add  12375  lo1mul  12376  mertenslem1  12616  sin01gt0  12746  cos01gt0  12747  sin02gt0  12748  bitsmod  12903  sadaddlem  12933  bezoutlem4  12996  mulgcd  13001  mulgcddvds  13059  rpmulgcd2  13060  isprm5  13067  rpexp  13075  rpdvds  13079  phimullem  13123  eulerthlem1  13125  eulerthlem2  13126  prmdiv  13129  prmdiveq  13130  pythagtriplem4  13148  pcpremul  13172  pcqmul  13182  pcdvdstr  13204  pcgcd1  13205  pcadd  13213  pockthlem  13228  prmreclem2  13240  4sqlem8  13268  4sqlem10  13270  4sqlem14  13281  4sqlem16  13283  ramub1lem1  13349  ramub1lem2  13350  iscatd2  13861  lattrd  14442  latledi  14473  mulgass  14875  gaorber  15040  efgredlem  15334  odadd2  15419  dmdprdpr  15562  ablfacrp2  15580  ablfac1b  15583  ablfac1eu  15586  pgpfac1  15593  gsumbagdiaglem  16395  znunit  16799  neiptoptop  17150  lmcnp  17322  txcls  17589  txlly  17621  txnlly  17622  tx1stc  17635  alexsubALTlem1  18031  prdsmet  18353  blin2  18412  blcvx  18782  tgqioo  18784  metnrmlem3  18844  iscmet3lem2  19198  ovolmge0  19326  ovolunlem2  19347  mbfi1flimlem  19567  mbfmullem  19570  itg2add  19604  dvlip2  19832  dvge0  19843  dvcvx  19857  dvfsumabs  19860  plyadd  20089  plymul  20090  dgrlb  20108  plydivlem4  20166  vieta1lem2  20181  ulmdvlem3  20271  sinq12gt0  20368  logdivlti  20468  fsumharmonic  20803  fsumdvdsdiaglem  20921  dvdsmulf1o  20932  logfacubnd  20958  perfectlem1  20966  dchrptlem2  21002  lgsmod  21058  2sqlem3  21103  2sqlem5  21105  2sqlem8  21109  dchrisum0flblem2  21156  pntibndlem2  21238  pntlemr  21249  pntlemp  21257  chscllem2  23093  chscllem4  23095  nmopge0  23367  nmfnge0  23383  nmoptrii  23550  staddi  23702  stadd3i  23704  atcvatlem  23841  supssd  24051  xrofsup  24079  xrge0addgt0  24167  ofldmul  24192  esumpmono  24422  erdszelem8  24837  txscon  24881  cvmlift2lem10  24952  cvmlift3lem7  24965  ghomgsg  25057  relexpsucl  25085  relexpcnv  25086  relexpdm  25088  relexprn  25089  rtrclreclem.trans  25099  dvdspw  25317  dfon2lem6  25358  dfon2lem8  25360  cgrtr4d  25823  cgrtrand  25831  cgrtr3and  25833  cgrextendand  25847  btwnexch3and  25859  btwnexchand  25864  linecgrand  25920  endofsegidand  25924  btwnconn1lem4  25928  btwnconn1lem8  25932  btwnconn1lem11  25935  btwnconn1lem12  25936  brsegle2  25947  seglecgr12im  25948  segleantisym  25953  colinbtwnle  25956  broutsideof2  25960  outsideoftr  25967  outsidele  25970  lineelsb2  25986  linethru  25991  mbfresfi  26152  gtinf  26212  ismrcd2  26643  pellqrex  26832  jm2.17b  26916  dvdsacongtr  26939  jm2.26lem3  26962  jm2.27a  26966  jm2.27c  26968  fnwe2lem2  27016  psgnunilem4  27288  addrcom  27547  stoweidlem15  27631  stoweidlem26  27642  stoweidlem28  27644  stoweidlem32  27648  stoweidlem44  27660  bnj1098  28860  bnj1110  29057  bnj1121  29060  lcvnbtwn2  29510  lcvnbtwn3  29511  lcvexchlem4  29520  omlfh1N  29741  atlen0  29793  atlatmstc  29802  cvratlem  29903  lnnat  29909  2atlt  29921  athgt  29938  1cvratex  29955  ps-2  29960  llncmp  30004  llncvrlpln  30040  lplncmp  30044  lplncvrlvol  30098  lvolcmp  30099  dalemcea  30142  dalem-cly  30153  dalem10  30155  dalem17  30162  dalem25  30180  dalem38  30192  dalem44  30198  dalem55  30209  2atm2atN  30267  cdlema1N  30273  paddasslem5  30306  dalawlem3  30355  dalawlem7  30359  dalawlem11  30363  dalawlem12  30364  lhp0lt  30485  4atexlemc  30551  cdlemg33a  31188  cdlemg33  31193  cdlemk51  31435  dia2dimlem2  31548  dia2dimlem3  31549  dihmeetlem20N  31809
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator