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

Theorem mpand 681
Description: A deduction based on modus ponens. (Contributed by NM, 12-Dec-2004.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)
Hypotheses
Ref Expression
mpand.1  |-  ( ph  ->  ps )
mpand.2  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
Assertion
Ref Expression
mpand  |-  ( ph  ->  ( ch  ->  th )
)

Proof of Theorem mpand
StepHypRef Expression
1 mpand.1 . 2  |-  ( ph  ->  ps )
2 mpand.2 . . 3  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
32ancomsd 456 . 2  |-  ( ph  ->  ( ( ch  /\  ps )  ->  th )
)
41, 3mpan2d 680 1  |-  ( ph  ->  ( ch  ->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371
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 189  df-an 373
This theorem is referenced by:  mpani  682  mp2and  685  ecase2d  951  disjss3  4401  sotri2  5229  ovig  6418  orduniorsuc  6657  omopth2  7285  frfi  7816  ordunifi  7821  finsschain  7881  cantnfp1lem3  8185  cantnfp1  8186  p1le  10448  nnge1  10635  zltp1le  10986  gtndiv  11013  uzss  11179  eluzadd  11187  uzm1  11189  xrre2  11465  xrre3  11466  xrmaxlt  11476  xrmaxle  11478  xrsupsslem  11592  xrub  11597  supxrunb1  11605  elfzoext  11971  flflp1  12043  ceile  12076  seqf1olem1  12252  leexp2r  12330  expnlbnd2  12403  facavg  12486  ccat2s1fvw  12771  caubnd2  13420  limsupbnd1  13544  limsupbnd1OLD  13545  limsupbnd2  13546  limsupbnd2OLD  13547  rlim2lt  13561  rlim3  13562  o1co  13650  mulcn2  13659  cn1lem  13661  rlimo1  13680  climsqz  13704  climsqz2  13705  rlimsqzlem  13712  lo1le  13715  rlimno1  13717  climsup  13733  caucvgrlem2  13740  iseraltlem2  13749  iseralt  13751  fsumabs  13861  cvgcmp  13876  cvgcmpce  13878  isumltss  13906  cvgrat  13939  ruclem9  14290  ruclem12  14293  bitsfzolem  14407  bitsfzolemOLD  14408  bitsfzo  14409  sadcaddlem  14431  gcdeq  14520  algcvgblem  14536  algcvga  14538  lcmdvdsb  14578  lcmftp  14609  coprm  14657  coprmdvds  14659  eulerthlem2  14730  pclem  14788  infpn2  14857  prmreclem1  14860  prmreclem4  14863  ramtlecl  14951  prmgaplem7  15027  initoeu2  15911  lubval  16230  lublecllem  16234  glbval  16243  joinle  16260  latmlem1  16327  odmulg  17207  efginvrel2  17377  pgpfac1lem5  17712  chfacfscmul0  19882  chfacfpmmul0  19886  1stccnp  20477  qustgplem  21135  imasdsf1olem  21388  bldisj  21413  xbln0  21429  prdsbl  21506  metss2lem  21526  stdbdxmet  21530  ngptgp  21644  nghmcn  21766  icoopnst  21967  iocopnst  21968  cnllycmp  21984  iscau3  22248  cmetcaulem  22258  iscmet3lem1  22261  bcthlem4  22295  ovollb2lem  22441  ovolicc2lem3  22472  voliunlem3  22505  volcn  22564  itg10a  22668  itg1ge0a  22669  dvcnvrelem1  22969  dvfsumrlim  22983  itgsubst  23001  ulmcn  23354  ulmdvlem3  23357  mtest  23359  tanord  23487  emcllem6  23926  ftalem2  23998  chtub  24140  fsumvma2  24142  vmasum  24144  chpchtsum  24147  bcmono  24205  bclbnd  24208  bposlem1  24212  bposlem5  24216  bposlem6  24217  lgsne0  24261  chtppilim  24313  dchrisumlem3  24329  pntrsumbnd2  24405  pntlemf  24443  pntlem3  24447  pntleml  24449  redwlklem  25335  eupath2  25708  grpoidinvlem3  25934  grpoideu  25937  vacn  26330  blocni  26446  ubthlem2  26513  chscllem2  27291  lnconi  27686  pjnmopi  27801  atomli  28035  sumdmdlem2  28072  cdj3lem2b  28090  xraddge02  28336  dfon2lem5  30433  dfon2lem6  30434  cgrcoml  30763  btwnconn2  30869  ltflcei  31933  poimirlem2  31942  poimirlem18  31958  poimirlem22  31962  poimirlem23  31963  poimirlem26  31966  poimirlem29  31969  poimirlem30  31970  poimirlem32  31972  heicant  31975  mblfinlem3  31979  mblfinlem4  31980  itg2addnclem  31993  itg2addnc  31996  bddiblnc  32012  ftc1anclem6  32022  ftc1anc  32025  mettrifi  32086  geomcau  32088  equivbnd  32122  heibor1lem  32141  bfplem1  32154  bfplem2  32155  rrncmslem  32164  divrngidl  32261  lecmtN  32822  cvrletrN  32839  llnnleat  33078  lplnnle2at  33106  lvolnle3at  33147  dalem21  33259  cdlemblem  33358  osumcllem11N  33531  pexmidlem8N  33542  lhpmcvr4N  33591  cdleme32b  34009  cdleme35fnpq  34016  cdleme48bw  34069  cdlemf1  34128  cdlemg2fv2  34167  cdlemg7fvbwN  34174  cdlemg27b  34263  tendoeq2  34341  dia2dimlem1  34632  dihord6apre  34824  dihord5apre  34830  dihglbcpreN  34868  dochnel2  34960  dihjat1lem  34996  dochexmidlem8  35035  mapdordlem2  35205  frege124d  36353  climinf  37684  climinfOLD  37685  iccpartlt  38738  gcdzeq  38793  bgoldbtbndlem3  38902  bgoldbtbndlem4  38903  tgoldbach  38911  fpropnf1  39036  2ffzoeq  39064  fllog2  40432  dignn0ldlem  40466
  Copyright terms: Public domain W3C validator