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

Theorem mp2and 679
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 675 . 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:  reu2eqd  3293  ssnelpssd  3884  tfisi  6664  tfindsg2  6667  mpt2sn  6864  smoord  7026  oelimcl  7239  oeeui  7241  nnawordex  7276  omabs  7286  ertrd  7317  omxpenlem  7608  ixpfi2  7807  supmax  7914  oismo  7954  cantnflem1c  8095  cantnflem1  8097  cantnflem3  8099  cantnflem1cOLD  8118  cantnflem1OLD  8120  cantnflem3OLD  8121  infxpenc2  8388  infxpenc2OLD  8392  axdc2lem  8817  r1limwun  9103  letrd  9727  lelttrd  9728  ltletrd  9730  lttrd  9731  le2addd  10159  le2subd  10160  ltleaddd  10161  leltaddd  10162  lt2subd  10164  ltmul12a  10387  lemul12ad  10477  lemul12bd  10478  lt2halvesd  10775  uzind  10941  uztrn  11087  xrlttrd  11351  xrlelttrd  11352  xrltletrd  11353  xrletrd  11354  supxrunb1  11500  supxrunb2  11501  ixxun  11534  ixxss1  11536  ixxss2  11537  ixxss12  11538  seqf1o  12104  faclbnd3  12325  sqrlem1  13026  sqrlem4  13029  sqrlem7  13032  abs3lemd  13241  rlimcn2  13362  o1of2  13384  lo1add  13398  lo1mul  13399  modfsummod  13557  mertenslem1  13645  sin01gt0  13775  cos01gt0  13776  sin02gt0  13777  bitsmod  13934  sadaddlem  13964  bezoutlem4  14027  mulgcd  14032  mulgcddvds  14093  rpmulgcd2  14094  isprm5  14101  rpexp  14109  rpdvds  14113  phimullem  14157  eulerthlem1  14159  eulerthlem2  14160  prmdiv  14163  prmdiveq  14164  pythagtriplem4  14191  pcpremul  14215  pcqmul  14225  pcdvdstr  14247  pcgcd1  14248  pcadd  14256  pockthlem  14271  prmreclem2  14283  4sqlem8  14311  4sqlem10  14313  4sqlem14  14324  4sqlem16  14326  ramub1lem1  14392  ramub1lem2  14393  iscatd2  14925  joinval  15481  meetval  15495  lattrd  15534  latledi  15565  mulgass  15965  gaorber  16134  psgnunilem4  16311  efgredlem  16554  odadd2  16641  dmdprdpr  16881  ablfacrp2  16901  ablfac1b  16904  ablfac1eu  16907  pgpfac1  16914  gsumbagdiaglem  17791  znunit  18362  mdetunilem1  18874  mdetunilem4  18877  mdetunilem9  18882  neiptoptop  19391  lmcnp  19564  txcls  19833  txlly  19865  txnlly  19866  tx1stc  19879  alexsubALTlem1  20275  prdsmet  20601  blin2  20660  blcvx  21031  tgqioo  21033  metnrmlem3  21093  iscmet3lem2  21459  ovolmge0  21616  ovolunlem2  21637  mbfi1flimlem  21857  mbfmullem  21860  itg2add  21894  dvlip2  22124  dvge0  22135  dvcvx  22149  dvfsumabs  22152  plyadd  22342  plymul  22343  dgrlb  22361  plydivlem4  22419  vieta1lem2  22434  ulmdvlem3  22524  sinq12gt0  22626  logdivlti  22726  fsumharmonic  23062  fsumdvdsdiaglem  23180  dvdsmulf1o  23191  logfacubnd  23217  perfectlem1  23225  dchrptlem2  23261  lgsmod  23317  2sqlem3  23362  2sqlem5  23364  2sqlem8  23368  dchrisum0flblem2  23415  pntibndlem2  23497  pntlemr  23508  pntlemp  23516  axtgpasch  23585  axtgupdim2  23590  wwlknredwwlkn  24388  wwlkextsur  24393  ex-natded5.2-2  24789  chscllem2  26218  chscllem4  26220  nmopge0  26492  nmfnge0  26508  nmoptrii  26675  staddi  26827  stadd3i  26829  atcvatlem  26966  supssd  27185  xrofsup  27236  xrge0addgt0  27329  archiabllem2c  27387  esumpmono  27711  erdszelem8  28268  txscon  28312  cvmlift2lem10  28383  cvmlift3lem7  28396  ghomgsg  28494  relexpsucl  28516  relexpcnv  28517  relexpdm  28519  relexprn  28520  rtrclreclem.trans  28530  dvdspw  28738  dfon2lem6  28783  dfon2lem8  28785  cgrtr4d  29198  cgrtrand  29206  cgrtr3and  29208  cgrextendand  29222  btwnexch3and  29234  btwnexchand  29239  linecgrand  29295  endofsegidand  29299  btwnconn1lem4  29303  btwnconn1lem8  29307  btwnconn1lem11  29310  btwnconn1lem12  29311  brsegle2  29322  seglecgr12im  29323  segleantisym  29328  colinbtwnle  29331  broutsideof2  29335  outsideoftr  29342  outsidele  29345  lineelsb2  29361  linethru  29366  heicant  29613  mbfresfi  29625  ftc1anclem6  29659  gtinf  29701  ismrcd2  30222  pellqrex  30406  jm2.17b  30490  dvdsacongtr  30513  jm2.26lem3  30536  jm2.27a  30540  jm2.27c  30542  fnwe2lem2  30590  addrcom  30917  stoweidlem15  31270  stoweidlem26  31281  stoweidlem28  31283  stoweidlem32  31287  stoweidlem44  31299  lcoss  31985  islindeps2  32032  isldepslvec2  32034  bnj1098  32796  bnj1110  32992  bnj1121  32995  riotasv2d  33635  lcvnbtwn2  33699  lcvnbtwn3  33700  lcvexchlem4  33709  omlfh1N  33930  atlen0  33982  atlatmstc  33991  cvratlem  34092  lnnat  34098  2atlt  34110  athgt  34127  1cvratex  34144  ps-2  34149  llncmp  34193  llncvrlpln  34229  lplncmp  34233  lplncvrlvol  34287  lvolcmp  34288  dalemcea  34331  dalem-cly  34342  dalem10  34344  dalem17  34351  dalem25  34369  dalem38  34381  dalem44  34387  dalem55  34398  2atm2atN  34456  cdlema1N  34462  paddasslem5  34495  dalawlem3  34544  dalawlem7  34548  dalawlem11  34552  dalawlem12  34553  lhp0lt  34674  4atexlemc  34740  cdlemg33a  35377  cdlemg33  35382  cdlemk51  35624  dia2dimlem2  35737  dia2dimlem3  35738  dihmeetlem20N  35998
  Copyright terms: Public domain W3C validator