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  3518  tfisi  4649  tfindsg2  4652  riotasv2d  6349  smoord  6382  oelimcl  6598  oeeui  6600  nnawordex  6635  omabs  6645  ertrd  6676  th3qlem1  6764  omxpenlem  6963  ixpfi2  7154  supmax  7216  oismo  7255  cantnflem1c  7389  cantnflem1  7391  cantnflem3  7393  infxpenc2  7649  isfin4-3  7941  axdc2lem  8074  r1limwun  8358  letrd  8973  lelttrd  8974  ltletrd  8976  lttrd  8977  le2addd  9390  le2subd  9391  ltleaddd  9392  leltaddd  9393  lt2subd  9395  ltmul12a  9612  lemul12ad  9699  lemul12bd  9700  lt2halvesd  9959  uzind  10103  uztrn  10244  xrlttrd  10490  xrlelttrd  10491  xrltletrd  10492  xrletrd  10493  supxrunb1  10638  supxrunb2  10639  ixxun  10672  ixxss1  10674  ixxss2  10675  ixxss12  10676  seqf1o  11087  faclbnd3  11305  sqrlem1  11728  sqrlem4  11731  sqrlem7  11734  abs3lemd  11943  rlimcn2  12064  o1of2  12086  lo1add  12100  lo1mul  12101  mertenslem1  12340  sin01gt0  12470  cos01gt0  12471  sin02gt0  12472  bitsmod  12627  sadaddlem  12657  bezoutlem4  12720  mulgcd  12725  mulgcddvds  12783  rpmulgcd2  12784  isprm5  12791  rpexp  12799  rpdvds  12803  phimullem  12847  eulerthlem1  12849  eulerthlem2  12850  prmdiv  12853  prmdiveq  12854  pythagtriplem4  12872  pcpremul  12896  pcqmul  12906  pcdvdstr  12928  pcgcd1  12929  pcadd  12937  pockthlem  12952  prmreclem2  12964  4sqlem8  12992  4sqlem10  12994  4sqlem14  13005  4sqlem16  13007  ramub1lem1  13073  ramub1lem2  13074  iscatd2  13583  lattrd  14164  latledi  14195  mulgass  14597  gaorber  14762  efgredlem  15056  odadd2  15141  dmdprdpr  15284  ablfacrp2  15302  ablfac1b  15305  ablfac1eu  15308  pgpfac1lem1  15309  pgpfac1  15315  pgpfaclem2  15317  gsumbagdiaglem  16121  znunit  16517  lmcnp  17032  txcls  17299  txlly  17330  txnlly  17331  tx1stc  17344  alexsubALTlem1  17741  prdsmet  17934  blin2  17975  blcvx  18304  tgqioo  18306  metnrmlem3  18365  iscmet3lem2  18718  ovolmge0  18836  ovolunlem2  18857  mbfi1flimlem  19077  mbfmullem  19080  itg2add  19114  dvlip2  19342  dvge0  19353  dvcvx  19367  dvfsumabs  19370  plyadd  19599  plymul  19600  dgrlb  19618  plydivlem4  19676  vieta1lem2  19691  ulmdvlem3  19779  sinq12gt0  19875  logdivlti  19971  fsumharmonic  20305  fsumdvdsdiaglem  20423  dvdsmulf1o  20434  logfacubnd  20460  perfectlem1  20468  dchrptlem2  20504  lgsmod  20560  2sqlem3  20605  2sqlem5  20607  2sqlem8  20611  dchrisum0flblem2  20658  pntibndlem2  20740  pntlemr  20751  pntlemp  20759  ex-natded5.2-2  20792  chscllem2  22217  chscllem4  22219  nmopge0  22491  nmfnge0  22507  nmoptrii  22674  staddi  22826  stadd3i  22828  atcvatlem  22965  xrofsup  23255  esumpmono  23447  mbfmco2  23570  orvclteinc  23676  erdszelem8  23729  txscon  23772  cvmlift2lem10  23843  cvmlift3lem7  23856  ghomgsg  24000  relexpsucl  24028  relexpcnv  24029  relexpdm  24032  relexprn  24033  rtrclreclem.trans  24043  dvdspw  24103  dfon2lem6  24144  dfon2lem8  24146  cgrtr4d  24608  cgrtrand  24616  cgrtr3and  24618  cgrextendand  24632  btwnexch3and  24644  btwnexchand  24649  linecgrand  24705  endofsegidand  24709  btwnconn1lem4  24713  btwnconn1lem8  24717  btwnconn1lem11  24720  btwnconn1lem12  24721  brsegle2  24732  seglecgr12im  24733  segleantisym  24738  colinbtwnle  24741  broutsideof2  24745  outsideoftr  24752  outsidele  24755  lineelsb2  24771  linethru  24776  iri  25800  gtinf  26234  ismrcd2  26774  pellqrex  26964  jm2.17b  27048  dvdsacongtr  27071  jm2.26lem3  27094  jm2.27a  27098  jm2.27c  27100  fnwe2lem2  27148  psgnunilem4  27420  addrcom  27680  bnj1098  28815  bnj1110  29012  bnj1121  29015  lcvnbtwn2  29217  lcvnbtwn3  29218  lcvexchlem4  29227  omlfh1N  29448  atlen0  29500  atlatmstc  29509  cvratlem  29610  lnnat  29616  2atlt  29628  athgt  29645  1cvratex  29662  ps-2  29667  llncmp  29711  llncvrlpln  29747  lplncmp  29751  lplncvrlvol  29805  lvolcmp  29806  dalemcea  29849  dalem-cly  29860  dalem10  29862  dalem17  29869  dalem25  29887  dalem38  29899  dalem44  29905  dalem55  29916  2atm2atN  29974  cdlema1N  29980  paddasslem5  30013  dalawlem3  30062  dalawlem7  30066  dalawlem11  30070  dalawlem12  30071  lhp0lt  30192  4atexlemc  30258  cdlemg33a  30895  cdlemg33  30900  cdlemk51  31142  dia2dimlem2  31255  dia2dimlem3  31256  dihmeetlem20N  31516
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