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

Theorem mpand 657
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 441 . 2  |-  ( ph  ->  ( ( ch  /\  ps )  ->  th )
)
41, 3mpan2d 656 1  |-  ( ph  ->  ( ch  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  mpani  658  mp2and  661  ecase2d  907  disjss3  4171  orduniorsuc  4769  sotri2  5222  ovig  6154  omopth2  6786  frfi  7311  ordunifi  7316  finsschain  7371  cantnfp1lem3  7592  cantnfp1  7593  p1le  9809  nnge1  9982  zltp1le  10281  gtndiv  10303  uzss  10462  eluzadd  10470  uzm1  10472  xrre2  10714  xrre3  10715  xrmaxlt  10725  xrmaxle  10727  xrsupsslem  10841  xrub  10846  supxrunb1  10854  ceile  11190  seqf1olem1  11317  leexp2r  11392  expnlbnd2  11465  facavg  11547  caubnd2  12116  limsupbnd1  12231  limsupbnd2  12232  rlim2lt  12246  rlim3  12247  o1co  12335  mulcn2  12344  cn1lem  12346  rlimo1  12365  climsqz  12389  climsqz2  12390  rlimsqzlem  12397  lo1le  12400  rlimno1  12402  climsup  12418  caucvgrlem2  12423  iseraltlem2  12431  iseralt  12433  fsumabs  12535  cvgcmp  12550  cvgcmpce  12552  isumltss  12583  cvgrat  12615  ruclem9  12792  ruclem12  12795  bitsfzolem  12901  bitsfzo  12902  sadcaddlem  12924  gcdeq  13007  algcvgblem  13023  algcvga  13025  coprm  13055  coprmdvds  13057  eulerthlem2  13126  pclem  13167  infpn2  13236  prmreclem1  13239  prmreclem4  13242  ramtlecl  13323  lubid  14394  joinle  14405  latmlem1  14465  odmulg  15147  efginvrel2  15314  pgpfac1lem5  15592  1stccnp  17478  divstgplem  18103  imasdsf1olem  18356  bldisj  18381  xbln0  18397  prdsbl  18474  metss2lem  18494  stdbdxmet  18498  ngptgp  18630  nghmcn  18732  icoopnst  18917  iocopnst  18918  cnllycmp  18934  iscau3  19184  cmetcaulem  19194  iscmet3lem1  19197  bcthlem4  19233  ovollb2lem  19337  ovolicc2lem3  19368  voliunlem3  19399  volcn  19451  itg10a  19555  itg1ge0a  19556  dvcnvrelem1  19854  dvfsumrlim  19868  itgsubst  19886  ulmcn  20268  ulmdvlem3  20271  mtest  20273  tanord  20393  emcllem6  20792  ftalem2  20809  chtub  20949  fsumvma2  20951  vmasum  20953  chpchtsum  20956  bcmono  21014  bclbnd  21017  bposlem1  21021  bposlem5  21025  bposlem6  21026  lgsne0  21070  chtppilim  21122  dchrisumlem3  21138  pntrsumbnd2  21214  pntlemf  21252  pntlem3  21256  pntleml  21258  redwlklem  21558  eupath2  21655  grpoidinvlem3  21747  grpoideu  21750  vacn  22143  blocni  22259  ubthlem2  22326  chscllem2  23093  lnconi  23489  pjnmopi  23604  atomli  23838  sumdmdlem2  23875  cdj3lem2b  23893  xraddge02  24076  dfon2lem5  25357  dfon2lem6  25358  cgrcoml  25834  btwnconn2  25940  ltflcei  26140  lxflflp1  26142  mblfinlem2  26144  mblfinlem3  26145  itg2addnclem  26155  itg2addnc  26158  bddiblnc  26174  mettrifi  26353  geomcau  26355  equivbnd  26389  heibor1lem  26408  bfplem1  26421  bfplem2  26422  rrncmslem  26431  divrngidl  26528  climinf  27599  lecmtN  29739  cvrletrN  29756  llnnleat  29995  lplnnle2at  30023  lvolnle3at  30064  dalem21  30176  cdlemblem  30275  osumcllem11N  30448  pexmidlem8N  30459  lhpmcvr4N  30508  cdleme32b  30924  cdleme35fnpq  30931  cdleme48bw  30984  cdlemf1  31043  cdlemg2fv2  31082  cdlemg7fvbwN  31089  cdlemg27b  31178  tendoeq2  31256  dia2dimlem1  31547  dihord6apre  31739  dihord5apre  31745  dihglbcpreN  31783  dochnel2  31875  dihjat1lem  31911  dochexmidlem8  31950  mapdordlem2  32120
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