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

Theorem mp2and 660
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 656 . 2  |-  ( ph  ->  ( ch  ->  th )
)
51, 4mpd 14 1  |-  ( ph  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  ssnelpssd  3594  tfisi  4728  tfindsg2  4731  riotasv2d  6433  smoord  6466  oelimcl  6682  oeeui  6684  nnawordex  6719  omabs  6729  ertrd  6760  th3qlem1  6849  omxpenlem  7048  ixpfi2  7241  supmax  7303  oismo  7342  cantnflem1c  7476  cantnflem1  7478  cantnflem3  7480  infxpenc2  7736  isfin4-3  8028  axdc2lem  8161  r1limwun  8445  letrd  9060  lelttrd  9061  ltletrd  9063  lttrd  9064  le2addd  9477  le2subd  9478  ltleaddd  9479  leltaddd  9480  lt2subd  9482  ltmul12a  9699  lemul12ad  9786  lemul12bd  9787  lt2halvesd  10048  uzind  10192  uztrn  10333  xrlttrd  10579  xrlelttrd  10580  xrltletrd  10581  xrletrd  10582  supxrunb1  10727  supxrunb2  10728  ixxun  10761  ixxss1  10763  ixxss2  10764  ixxss12  10765  seqf1o  11176  faclbnd3  11395  sqrlem1  11818  sqrlem4  11821  sqrlem7  11824  abs3lemd  12033  rlimcn2  12154  o1of2  12176  lo1add  12190  lo1mul  12191  mertenslem1  12431  sin01gt0  12561  cos01gt0  12562  sin02gt0  12563  bitsmod  12718  sadaddlem  12748  bezoutlem4  12811  mulgcd  12816  mulgcddvds  12874  rpmulgcd2  12875  isprm5  12882  rpexp  12890  rpdvds  12894  phimullem  12938  eulerthlem1  12940  eulerthlem2  12941  prmdiv  12944  prmdiveq  12945  pythagtriplem4  12963  pcpremul  12987  pcqmul  12997  pcdvdstr  13019  pcgcd1  13020  pcadd  13028  pockthlem  13043  prmreclem2  13055  4sqlem8  13083  4sqlem10  13085  4sqlem14  13096  4sqlem16  13098  ramub1lem1  13164  ramub1lem2  13165  iscatd2  13676  lattrd  14257  latledi  14288  mulgass  14690  gaorber  14855  efgredlem  15149  odadd2  15234  dmdprdpr  15377  ablfacrp2  15395  ablfac1b  15398  ablfac1eu  15401  pgpfac1lem1  15402  pgpfac1  15408  pgpfaclem2  15410  gsumbagdiaglem  16214  znunit  16617  lmcnp  17132  txcls  17399  txlly  17430  txnlly  17431  tx1stc  17444  alexsubALTlem1  17837  prdsmet  18030  blin2  18071  blcvx  18400  tgqioo  18402  metnrmlem3  18462  iscmet3lem2  18816  ovolmge0  18934  ovolunlem2  18955  mbfi1flimlem  19175  mbfmullem  19178  itg2add  19212  dvlip2  19440  dvge0  19451  dvcvx  19465  dvfsumabs  19468  plyadd  19697  plymul  19698  dgrlb  19716  plydivlem4  19774  vieta1lem2  19789  ulmdvlem3  19879  sinq12gt0  19976  logdivlti  20076  fsumharmonic  20411  fsumdvdsdiaglem  20529  dvdsmulf1o  20540  logfacubnd  20566  perfectlem1  20574  dchrptlem2  20610  lgsmod  20666  2sqlem3  20711  2sqlem5  20713  2sqlem8  20717  dchrisum0flblem2  20764  pntibndlem2  20846  pntlemr  20857  pntlemp  20865  ex-natded5.2-2  20898  chscllem2  22325  chscllem4  22327  nmopge0  22599  nmfnge0  22615  nmoptrii  22782  staddi  22934  stadd3i  22936  atcvatlem  23073  xrofsup  23324  esumpmono  23735  mbfmco2  23879  orvclteinc  23982  erdszelem8  24133  txscon  24176  cvmlift2lem10  24247  cvmlift3lem7  24260  ghomgsg  24404  relexpsucl  24432  relexpcnv  24433  relexpdm  24436  relexprn  24437  rtrclreclem.trans  24447  dvdspw  24661  dfon2lem6  24702  dfon2lem8  24704  cgrtr4d  25167  cgrtrand  25175  cgrtr3and  25177  cgrextendand  25191  btwnexch3and  25203  btwnexchand  25208  linecgrand  25264  endofsegidand  25268  btwnconn1lem4  25272  btwnconn1lem8  25276  btwnconn1lem11  25279  btwnconn1lem12  25280  brsegle2  25291  seglecgr12im  25292  segleantisym  25297  colinbtwnle  25300  broutsideof2  25304  outsideoftr  25311  outsidele  25314  lineelsb2  25330  linethru  25335  gtinf  25558  ismrcd2  26097  pellqrex  26287  jm2.17b  26371  dvdsacongtr  26394  jm2.26lem3  26417  jm2.27a  26421  jm2.27c  26423  fnwe2lem2  26471  psgnunilem4  26743  addrcom  27003  bnj1098  28560  bnj1110  28757  bnj1121  28760  lcvnbtwn2  29269  lcvnbtwn3  29270  lcvexchlem4  29279  omlfh1N  29500  atlen0  29552  atlatmstc  29561  cvratlem  29662  lnnat  29668  2atlt  29680  athgt  29697  1cvratex  29714  ps-2  29719  llncmp  29763  llncvrlpln  29799  lplncmp  29803  lplncvrlvol  29857  lvolcmp  29858  dalemcea  29901  dalem-cly  29912  dalem10  29914  dalem17  29921  dalem25  29939  dalem38  29951  dalem44  29957  dalem55  29968  2atm2atN  30026  cdlema1N  30032  paddasslem5  30065  dalawlem3  30114  dalawlem7  30118  dalawlem11  30122  dalawlem12  30123  lhp0lt  30244  4atexlemc  30310  cdlemg33a  30947  cdlemg33  30952  cdlemk51  31194  dia2dimlem2  31307  dia2dimlem3  31308  dihmeetlem20N  31568
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 177  df-an 360
  Copyright terms: Public domain W3C validator