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  3552  tfisi  4686  tfindsg2  4689  riotasv2d  6391  smoord  6424  oelimcl  6640  oeeui  6642  nnawordex  6677  omabs  6687  ertrd  6718  th3qlem1  6807  omxpenlem  7006  ixpfi2  7199  supmax  7261  oismo  7300  cantnflem1c  7434  cantnflem1  7436  cantnflem3  7438  infxpenc2  7694  isfin4-3  7986  axdc2lem  8119  r1limwun  8403  letrd  9018  lelttrd  9019  ltletrd  9021  lttrd  9022  le2addd  9435  le2subd  9436  ltleaddd  9437  leltaddd  9438  lt2subd  9440  ltmul12a  9657  lemul12ad  9744  lemul12bd  9745  lt2halvesd  10006  uzind  10150  uztrn  10291  xrlttrd  10537  xrlelttrd  10538  xrltletrd  10539  xrletrd  10540  supxrunb1  10685  supxrunb2  10686  ixxun  10719  ixxss1  10721  ixxss2  10722  ixxss12  10723  seqf1o  11134  faclbnd3  11352  sqrlem1  11775  sqrlem4  11778  sqrlem7  11781  abs3lemd  11990  rlimcn2  12111  o1of2  12133  lo1add  12147  lo1mul  12148  mertenslem1  12387  sin01gt0  12517  cos01gt0  12518  sin02gt0  12519  bitsmod  12674  sadaddlem  12704  bezoutlem4  12767  mulgcd  12772  mulgcddvds  12830  rpmulgcd2  12831  isprm5  12838  rpexp  12846  rpdvds  12850  phimullem  12894  eulerthlem1  12896  eulerthlem2  12897  prmdiv  12900  prmdiveq  12901  pythagtriplem4  12919  pcpremul  12943  pcqmul  12953  pcdvdstr  12975  pcgcd1  12976  pcadd  12984  pockthlem  12999  prmreclem2  13011  4sqlem8  13039  4sqlem10  13041  4sqlem14  13052  4sqlem16  13054  ramub1lem1  13120  ramub1lem2  13121  iscatd2  13632  lattrd  14213  latledi  14244  mulgass  14646  gaorber  14811  efgredlem  15105  odadd2  15190  dmdprdpr  15333  ablfacrp2  15351  ablfac1b  15354  ablfac1eu  15357  pgpfac1lem1  15358  pgpfac1  15364  pgpfaclem2  15366  gsumbagdiaglem  16170  znunit  16573  lmcnp  17088  txcls  17355  txlly  17386  txnlly  17387  tx1stc  17400  alexsubALTlem1  17793  prdsmet  17986  blin2  18027  blcvx  18356  tgqioo  18358  metnrmlem3  18417  iscmet3lem2  18771  ovolmge0  18889  ovolunlem2  18910  mbfi1flimlem  19130  mbfmullem  19133  itg2add  19167  dvlip2  19395  dvge0  19406  dvcvx  19420  dvfsumabs  19423  plyadd  19652  plymul  19653  dgrlb  19671  plydivlem4  19729  vieta1lem2  19744  ulmdvlem3  19832  sinq12gt0  19928  logdivlti  20024  fsumharmonic  20358  fsumdvdsdiaglem  20476  dvdsmulf1o  20487  logfacubnd  20513  perfectlem1  20521  dchrptlem2  20557  lgsmod  20613  2sqlem3  20658  2sqlem5  20660  2sqlem8  20664  dchrisum0flblem2  20711  pntibndlem2  20793  pntlemr  20804  pntlemp  20812  ex-natded5.2-2  20845  chscllem2  22272  chscllem4  22274  nmopge0  22546  nmfnge0  22562  nmoptrii  22729  staddi  22881  stadd3i  22883  atcvatlem  23020  xrofsup  23272  esumpmono  23645  mbfmco2  23789  orvclteinc  23907  erdszelem8  24013  txscon  24056  cvmlift2lem10  24127  cvmlift3lem7  24140  ghomgsg  24284  relexpsucl  24312  relexpcnv  24313  relexpdm  24316  relexprn  24317  rtrclreclem.trans  24327  dvdspw  24488  dfon2lem6  24529  dfon2lem8  24531  cgrtr4d  24994  cgrtrand  25002  cgrtr3and  25004  cgrextendand  25018  btwnexch3and  25030  btwnexchand  25035  linecgrand  25091  endofsegidand  25095  btwnconn1lem4  25099  btwnconn1lem8  25103  btwnconn1lem11  25106  btwnconn1lem12  25107  brsegle2  25118  seglecgr12im  25119  segleantisym  25124  colinbtwnle  25127  broutsideof2  25131  outsideoftr  25138  outsidele  25141  lineelsb2  25157  linethru  25162  gtinf  25383  ismrcd2  25922  pellqrex  26112  jm2.17b  26196  dvdsacongtr  26219  jm2.26lem3  26242  jm2.27a  26246  jm2.27c  26248  fnwe2lem2  26296  psgnunilem4  26568  addrcom  26828  bnj1098  28326  bnj1110  28523  bnj1121  28526  lcvnbtwn2  29035  lcvnbtwn3  29036  lcvexchlem4  29045  omlfh1N  29266  atlen0  29318  atlatmstc  29327  cvratlem  29428  lnnat  29434  2atlt  29446  athgt  29463  1cvratex  29480  ps-2  29485  llncmp  29529  llncvrlpln  29565  lplncmp  29569  lplncvrlvol  29623  lvolcmp  29624  dalemcea  29667  dalem-cly  29678  dalem10  29680  dalem17  29687  dalem25  29705  dalem38  29717  dalem44  29723  dalem55  29734  2atm2atN  29792  cdlema1N  29798  paddasslem5  29831  dalawlem3  29880  dalawlem7  29884  dalawlem11  29888  dalawlem12  29889  lhp0lt  30010  4atexlemc  30076  cdlemg33a  30713  cdlemg33  30718  cdlemk51  30960  dia2dimlem2  31073  dia2dimlem3  31074  dihmeetlem20N  31334
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