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

Theorem mp2and 672
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 668 . 2  |-  ( ph  ->  ( ch  ->  th )
)
51, 4mpd 15 1  |-  ( ph  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  ssnelpssd  3731  tfisi  6458  tfindsg2  6461  smoord  6812  oelimcl  7027  oeeui  7029  nnawordex  7064  omabs  7074  ertrd  7105  th3qlem1  7194  omxpenlem  7400  ixpfi2  7597  supmax  7703  oismo  7742  cantnflem1c  7883  cantnflem1  7885  cantnflem3  7887  cantnflem1cOLD  7906  cantnflem1OLD  7908  cantnflem3OLD  7909  infxpenc2  8176  infxpenc2OLD  8180  axdc2lem  8605  r1limwun  8891  letrd  9516  lelttrd  9517  ltletrd  9519  lttrd  9520  le2addd  9945  le2subd  9946  ltleaddd  9947  leltaddd  9948  lt2subd  9950  ltmul12a  10173  lemul12ad  10263  lemul12bd  10264  lt2halvesd  10560  uzind  10721  uztrn  10865  xrlttrd  11121  xrlelttrd  11122  xrltletrd  11123  xrletrd  11124  supxrunb1  11270  supxrunb2  11271  ixxun  11304  ixxss1  11306  ixxss2  11307  ixxss12  11308  seqf1o  11831  faclbnd3  12052  sqrlem1  12716  sqrlem4  12719  sqrlem7  12722  abs3lemd  12931  rlimcn2  13052  o1of2  13074  lo1add  13088  lo1mul  13089  mertenslem1  13327  sin01gt0  13457  cos01gt0  13458  sin02gt0  13459  bitsmod  13615  sadaddlem  13645  bezoutlem4  13708  mulgcd  13713  mulgcddvds  13773  rpmulgcd2  13774  isprm5  13781  rpexp  13789  rpdvds  13793  phimullem  13837  eulerthlem1  13839  eulerthlem2  13840  prmdiv  13843  prmdiveq  13844  pythagtriplem4  13869  pcpremul  13893  pcqmul  13903  pcdvdstr  13925  pcgcd1  13926  pcadd  13934  pockthlem  13949  prmreclem2  13961  4sqlem8  13989  4sqlem10  13991  4sqlem14  14002  4sqlem16  14004  ramub1lem1  14070  ramub1lem2  14071  iscatd2  14602  joinval  15158  meetval  15172  lattrd  15211  latledi  15242  mulgass  15637  gaorber  15806  psgnunilem4  15983  efgredlem  16224  odadd2  16311  dmdprdpr  16522  ablfacrp2  16542  ablfac1b  16545  ablfac1eu  16548  pgpfac1  16555  gsumbagdiaglem  17379  znunit  17838  mdetunilem1  18260  mdetunilem4  18263  mdetunilem9  18268  neiptoptop  18577  lmcnp  18750  txcls  19019  txlly  19051  txnlly  19052  tx1stc  19065  alexsubALTlem1  19461  prdsmet  19787  blin2  19846  blcvx  20217  tgqioo  20219  metnrmlem3  20279  iscmet3lem2  20645  ovolmge0  20802  ovolunlem2  20823  mbfi1flimlem  21042  mbfmullem  21045  itg2add  21079  dvlip2  21309  dvge0  21320  dvcvx  21334  dvfsumabs  21337  plyadd  21570  plymul  21571  dgrlb  21589  plydivlem4  21647  vieta1lem2  21662  ulmdvlem3  21752  sinq12gt0  21854  logdivlti  21954  fsumharmonic  22290  fsumdvdsdiaglem  22408  dvdsmulf1o  22419  logfacubnd  22445  perfectlem1  22453  dchrptlem2  22489  lgsmod  22545  2sqlem3  22590  2sqlem5  22592  2sqlem8  22596  dchrisum0flblem2  22643  pntibndlem2  22725  pntlemr  22736  pntlemp  22744  axtgpasch  22813  axtgupdim2  22817  ex-natded5.2-2  23435  chscllem2  24864  chscllem4  24866  nmopge0  25138  nmfnge0  25154  nmoptrii  25321  staddi  25473  stadd3i  25475  atcvatlem  25612  supssd  25828  xrofsup  25878  xrge0addgt0  25977  archiabllem2c  26036  esumpmono  26382  erdszelem8  26934  txscon  26978  cvmlift2lem10  27049  cvmlift3lem7  27062  ghomgsg  27159  relexpsucl  27181  relexpcnv  27182  relexpdm  27184  relexprn  27185  rtrclreclem.trans  27195  dvdspw  27403  dfon2lem6  27448  dfon2lem8  27450  cgrtr4d  27863  cgrtrand  27871  cgrtr3and  27873  cgrextendand  27887  btwnexch3and  27899  btwnexchand  27904  linecgrand  27960  endofsegidand  27964  btwnconn1lem4  27968  btwnconn1lem8  27972  btwnconn1lem11  27975  btwnconn1lem12  27976  brsegle2  27987  seglecgr12im  27988  segleantisym  27993  colinbtwnle  27996  broutsideof2  28000  outsideoftr  28007  outsidele  28010  lineelsb2  28026  linethru  28031  heicant  28270  mbfresfi  28282  ftc1anclem6  28316  gtinf  28358  ismrcd2  28880  pellqrex  29065  jm2.17b  29149  dvdsacongtr  29172  jm2.26lem3  29195  jm2.27a  29199  jm2.27c  29201  fnwe2lem2  29249  addrcom  29576  stoweidlem15  29656  stoweidlem26  29667  stoweidlem28  29669  stoweidlem32  29673  stoweidlem44  29685  modfsummod  30091  wwlknredwwlkn  30204  wwlkextsur  30209  mpt2sn  30568  lcoss  30679  islindeps2  30726  isldepslvec2  30728  bnj1098  31479  bnj1110  31675  bnj1121  31678  riotasv2d  32181  lcvnbtwn2  32245  lcvnbtwn3  32246  lcvexchlem4  32255  omlfh1N  32476  atlen0  32528  atlatmstc  32537  cvratlem  32638  lnnat  32644  2atlt  32656  athgt  32673  1cvratex  32690  ps-2  32695  llncmp  32739  llncvrlpln  32775  lplncmp  32779  lplncvrlvol  32833  lvolcmp  32834  dalemcea  32877  dalem-cly  32888  dalem10  32890  dalem17  32897  dalem25  32915  dalem38  32927  dalem44  32933  dalem55  32944  2atm2atN  33002  cdlema1N  33008  paddasslem5  33041  dalawlem3  33090  dalawlem7  33094  dalawlem11  33098  dalawlem12  33099  lhp0lt  33220  4atexlemc  33286  cdlemg33a  33923  cdlemg33  33928  cdlemk51  34170  dia2dimlem2  34283  dia2dimlem3  34284  dihmeetlem20N  34544
  Copyright terms: Public domain W3C validator