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  3282  ssnelpssd  3877  tfisi  6678  tfindsg2  6681  mpt2sn  6876  smoord  7038  oelimcl  7251  oeeui  7253  nnawordex  7288  omabs  7298  ertrd  7329  omxpenlem  7620  ixpfi2  7820  supmaxOLD  7928  oismo  7968  cantnflem1c  8109  cantnflem1  8111  cantnflem3  8113  cantnflem1cOLD  8132  cantnflem1OLD  8134  cantnflem3OLD  8135  infxpenc2  8402  infxpenc2OLD  8406  axdc2lem  8831  r1limwun  9117  letrd  9742  lelttrd  9743  ltletrd  9745  lttrd  9746  le2addd  10176  le2subd  10177  ltleaddd  10178  leltaddd  10179  lt2subd  10181  ltmul12a  10404  lemul12ad  10494  lemul12bd  10495  lt2halvesd  10792  uzind  10960  uztrn  11106  xrlttrd  11371  xrlelttrd  11372  xrltletrd  11373  xrletrd  11374  supxrunb1  11520  supxrunb2  11521  ixxun  11554  ixxss1  11556  ixxss2  11557  ixxss12  11558  seqf1o  12127  faclbnd3  12349  sqrlem1  13055  sqrlem4  13058  sqrlem7  13061  abs3lemd  13271  rlimcn2  13392  o1of2  13414  lo1add  13428  lo1mul  13429  modfsummod  13587  mertenslem1  13672  sin01gt0  13802  cos01gt0  13803  sin02gt0  13804  dvds2subd  13894  bitsmod  13963  sadaddlem  13993  bezoutlem4  14056  mulgcd  14061  mulgcddvds  14122  rpmulgcd2  14123  isprm5  14130  rpexp  14138  rpdvds  14142  phimullem  14186  eulerthlem1  14188  eulerthlem2  14189  prmdiv  14192  prmdiveq  14193  pythagtriplem4  14220  pcpremul  14244  pcqmul  14254  pcdvdstr  14276  pcgcd1  14277  pcadd  14285  pockthlem  14300  prmreclem2  14312  4sqlem8  14340  4sqlem10  14342  4sqlem14  14353  4sqlem16  14355  ramub1lem1  14421  ramub1lem2  14422  iscatd2  14955  joinval  15509  meetval  15523  lattrd  15562  latledi  15593  mulgass  16046  gaorber  16220  psgnunilem4  16396  efgredlem  16639  odadd2  16729  dmdprdpr  16972  ablfacrp2  16992  ablfac1b  16995  ablfac1eu  16998  pgpfac1  17005  gsumbagdiaglem  17901  znunit  18475  mdetunilem1  18987  mdetunilem4  18990  mdetunilem9  18995  neiptoptop  19505  lmcnp  19678  txcls  19978  txlly  20010  txnlly  20011  tx1stc  20024  alexsubALTlem1  20420  prdsmet  20746  blin2  20805  blcvx  21176  tgqioo  21178  metnrmlem3  21238  iscmet3lem2  21604  ovolmge0  21761  ovolunlem2  21782  mbfi1flimlem  22002  mbfmullem  22005  itg2add  22039  dvlip2  22269  dvge0  22280  dvcvx  22294  dvfsumabs  22297  plyadd  22487  plymul  22488  dgrlb  22506  plydivlem4  22564  vieta1lem2  22579  ulmdvlem3  22669  sinq12gt0  22772  logdivlti  22877  fsumharmonic  23213  fsumdvdsdiaglem  23331  dvdsmulf1o  23342  logfacubnd  23368  perfectlem1  23376  dchrptlem2  23412  lgsmod  23468  2sqlem3  23513  2sqlem5  23515  2sqlem8  23519  dchrisum0flblem2  23566  pntibndlem2  23648  pntlemr  23659  pntlemp  23667  axtgpasch  23736  axtgupdim2  23741  wwlknredwwlkn  24598  wwlkextsur  24603  ex-natded5.2-2  24998  chscllem2  26428  chscllem4  26430  nmopge0  26702  nmfnge0  26718  nmoptrii  26885  staddi  27037  stadd3i  27039  atcvatlem  27176  supssd  27399  xrofsup  27454  2sqmod  27509  xrge0addgt0  27554  archiabllem2c  27612  orngmul  27666  esumpmono  27958  signstfvneq0  28402  erdszelem8  28515  txscon  28559  cvmlift2lem10  28630  cvmlift3lem7  28643  ghomgsg  28906  relexpsucl  28928  relexpcnv  28929  relexpdm  28931  relexprn  28932  rtrclreclem.trans  28942  dvdspw  29150  dfon2lem6  29195  dfon2lem8  29197  cgrtr4d  29610  cgrtrand  29618  cgrtr3and  29620  cgrextendand  29634  btwnexch3and  29646  btwnexchand  29651  linecgrand  29707  endofsegidand  29711  btwnconn1lem4  29715  btwnconn1lem8  29719  btwnconn1lem11  29722  btwnconn1lem12  29723  brsegle2  29734  seglecgr12im  29735  segleantisym  29740  colinbtwnle  29743  broutsideof2  29747  outsideoftr  29754  outsidele  29757  lineelsb2  29773  linethru  29778  heicant  30024  mbfresfi  30036  ftc1anclem6  30070  gtinf  30112  ismrcd2  30606  pellqrex  30790  jm2.17b  30874  dvdsacongtr  30897  jm2.26lem3  30918  jm2.27a  30922  jm2.27c  30924  fnwe2lem2  30972  gcddvdslcm  31184  lcmgcdeq  31192  addrcom  31338  0ellimcdiv  31563  stoweidlem15  31686  stoweidlem26  31697  stoweidlem28  31699  stoweidlem32  31703  stoweidlem44  31715  copisnmnd  32334  assintopass  32375  lcoss  32772  islindeps2  32819  isldepslvec2  32821  bnj1098  33575  bnj1110  33771  bnj1121  33774  riotasv2d  34428  lcvnbtwn2  34492  lcvnbtwn3  34493  lcvexchlem4  34502  omlfh1N  34723  atlen0  34775  atlatmstc  34784  cvratlem  34885  lnnat  34891  2atlt  34903  athgt  34920  1cvratex  34937  ps-2  34942  llncmp  34986  llncvrlpln  35022  lplncmp  35026  lplncvrlvol  35080  lvolcmp  35081  dalemcea  35124  dalem-cly  35135  dalem10  35137  dalem17  35144  dalem25  35162  dalem38  35174  dalem44  35180  dalem55  35191  2atm2atN  35249  cdlema1N  35255  paddasslem5  35288  dalawlem3  35337  dalawlem7  35341  dalawlem11  35345  dalawlem12  35346  lhp0lt  35467  4atexlemc  35533  cdlemg33a  36172  cdlemg33  36177  cdlemk51  36419  dia2dimlem2  36532  dia2dimlem3  36533  dihmeetlem20N  36793  fco2d  37644
  Copyright terms: Public domain W3C validator