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

Theorem mp2and 661
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 657 . 2  |-  ( ph  ->  ( ch  ->  th )
)
51, 4mpd 15 1  |-  ( ph  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  ssnelpssd  3692  tfisi  4838  tfindsg2  4841  riotasv2d  6594  smoord  6627  oelimcl  6843  oeeui  6845  nnawordex  6880  omabs  6890  ertrd  6921  th3qlem1  7010  omxpenlem  7209  ixpfi2  7405  supmax  7470  oismo  7509  cantnflem1c  7643  cantnflem1  7645  cantnflem3  7647  infxpenc2  7903  axdc2lem  8328  r1limwun  8611  letrd  9227  lelttrd  9228  ltletrd  9230  lttrd  9231  le2addd  9644  le2subd  9645  ltleaddd  9646  leltaddd  9647  lt2subd  9649  ltmul12a  9866  lemul12ad  9953  lemul12bd  9954  lt2halvesd  10215  uzind  10361  uztrn  10502  xrlttrd  10749  xrlelttrd  10750  xrltletrd  10751  xrletrd  10752  supxrunb1  10898  supxrunb2  10899  ixxun  10932  ixxss1  10934  ixxss2  10935  ixxss12  10936  seqf1o  11364  faclbnd3  11583  sqrlem1  12048  sqrlem4  12051  sqrlem7  12054  abs3lemd  12263  rlimcn2  12384  o1of2  12406  lo1add  12420  lo1mul  12421  mertenslem1  12661  sin01gt0  12791  cos01gt0  12792  sin02gt0  12793  bitsmod  12948  sadaddlem  12978  bezoutlem4  13041  mulgcd  13046  mulgcddvds  13104  rpmulgcd2  13105  isprm5  13112  rpexp  13120  rpdvds  13124  phimullem  13168  eulerthlem1  13170  eulerthlem2  13171  prmdiv  13174  prmdiveq  13175  pythagtriplem4  13193  pcpremul  13217  pcqmul  13227  pcdvdstr  13249  pcgcd1  13250  pcadd  13258  pockthlem  13273  prmreclem2  13285  4sqlem8  13313  4sqlem10  13315  4sqlem14  13326  4sqlem16  13328  ramub1lem1  13394  ramub1lem2  13395  iscatd2  13906  lattrd  14487  latledi  14518  mulgass  14920  gaorber  15085  efgredlem  15379  odadd2  15464  dmdprdpr  15607  ablfacrp2  15625  ablfac1b  15628  ablfac1eu  15631  pgpfac1  15638  gsumbagdiaglem  16440  znunit  16844  neiptoptop  17195  lmcnp  17368  txcls  17636  txlly  17668  txnlly  17669  tx1stc  17682  alexsubALTlem1  18078  prdsmet  18400  blin2  18459  blcvx  18829  tgqioo  18831  metnrmlem3  18891  iscmet3lem2  19245  ovolmge0  19373  ovolunlem2  19394  mbfi1flimlem  19614  mbfmullem  19617  itg2add  19651  dvlip2  19879  dvge0  19890  dvcvx  19904  dvfsumabs  19907  plyadd  20136  plymul  20137  dgrlb  20155  plydivlem4  20213  vieta1lem2  20228  ulmdvlem3  20318  sinq12gt0  20415  logdivlti  20515  fsumharmonic  20850  fsumdvdsdiaglem  20968  dvdsmulf1o  20979  logfacubnd  21005  perfectlem1  21013  dchrptlem2  21049  lgsmod  21105  2sqlem3  21150  2sqlem5  21152  2sqlem8  21156  dchrisum0flblem2  21203  pntibndlem2  21285  pntlemr  21296  pntlemp  21304  chscllem2  23140  chscllem4  23142  nmopge0  23414  nmfnge0  23430  nmoptrii  23597  staddi  23749  stadd3i  23751  atcvatlem  23888  supssd  24098  xrofsup  24126  xrge0addgt0  24214  ofldmul  24239  esumpmono  24469  erdszelem8  24884  txscon  24928  cvmlift2lem10  24999  cvmlift3lem7  25012  ghomgsg  25104  relexpsucl  25132  relexpcnv  25133  relexpdm  25135  relexprn  25136  rtrclreclem.trans  25146  dvdspw  25369  dfon2lem6  25415  dfon2lem8  25417  cgrtr4d  25919  cgrtrand  25927  cgrtr3and  25929  cgrextendand  25943  btwnexch3and  25955  btwnexchand  25960  linecgrand  26016  endofsegidand  26020  btwnconn1lem4  26024  btwnconn1lem8  26028  btwnconn1lem11  26031  btwnconn1lem12  26032  brsegle2  26043  seglecgr12im  26044  segleantisym  26049  colinbtwnle  26052  broutsideof2  26056  outsideoftr  26063  outsidele  26066  lineelsb2  26082  linethru  26087  mbfresfi  26253  ftc1anclem6  26285  gtinf  26322  ismrcd2  26753  pellqrex  26942  jm2.17b  27026  dvdsacongtr  27049  jm2.26lem3  27072  jm2.27a  27076  jm2.27c  27078  fnwe2lem2  27126  psgnunilem4  27397  addrcom  27656  stoweidlem15  27740  stoweidlem26  27751  stoweidlem28  27753  stoweidlem32  27757  stoweidlem44  27769  bnj1098  29154  bnj1110  29351  bnj1121  29354  lcvnbtwn2  29825  lcvnbtwn3  29826  lcvexchlem4  29835  omlfh1N  30056  atlen0  30108  atlatmstc  30117  cvratlem  30218  lnnat  30224  2atlt  30236  athgt  30253  1cvratex  30270  ps-2  30275  llncmp  30319  llncvrlpln  30355  lplncmp  30359  lplncvrlvol  30413  lvolcmp  30414  dalemcea  30457  dalem-cly  30468  dalem10  30470  dalem17  30477  dalem25  30495  dalem38  30507  dalem44  30513  dalem55  30524  2atm2atN  30582  cdlema1N  30588  paddasslem5  30621  dalawlem3  30670  dalawlem7  30674  dalawlem11  30678  dalawlem12  30679  lhp0lt  30800  4atexlemc  30866  cdlemg33a  31503  cdlemg33  31508  cdlemk51  31750  dia2dimlem2  31863  dia2dimlem3  31864  dihmeetlem20N  32124
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 178  df-an 361
  Copyright terms: Public domain W3C validator