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

Theorem mpand 675
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 454 . 2  |-  ( ph  ->  ( ( ch  /\  ps )  ->  th )
)
41, 3mpan2d 674 1  |-  ( ph  ->  ( ch  ->  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:  mpani  676  mp2and  679  ecase2d  938  disjss3  4432  sotri2  5382  ovig  6405  orduniorsuc  6646  omopth2  7231  frfi  7763  ordunifi  7768  finsschain  7825  cantnfp1lem3  8097  cantnfp1  8098  cantnfp1lem3OLD  8123  cantnfp1OLD  8124  p1le  10386  nnge1  10563  zltp1le  10914  gtndiv  10941  uzss  11105  eluzadd  11113  uzm1  11115  xrre2  11375  xrre3  11376  xrmaxlt  11386  xrmaxle  11388  xrsupsslem  11502  xrub  11507  supxrunb1  11515  flflp1  11918  ceile  11950  seqf1olem1  12120  leexp2r  12197  expnlbnd2  12271  facavg  12353  caubnd2  13164  limsupbnd1  13279  limsupbnd2  13280  rlim2lt  13294  rlim3  13295  o1co  13383  mulcn2  13392  cn1lem  13394  rlimo1  13413  climsqz  13437  climsqz2  13438  rlimsqzlem  13445  lo1le  13448  rlimno1  13450  climsup  13466  caucvgrlem2  13471  iseraltlem2  13479  iseralt  13481  fsumabs  13589  cvgcmp  13604  cvgcmpce  13606  isumltss  13634  cvgrat  13666  ruclem9  13843  ruclem12  13846  bitsfzolem  13956  bitsfzo  13957  sadcaddlem  13979  gcdeq  14062  algcvgblem  14078  algcvga  14080  coprm  14113  coprmdvds  14115  eulerthlem2  14184  pclem  14234  infpn2  14303  prmreclem1  14306  prmreclem4  14309  ramtlecl  14390  lubval  15483  lublecllem  15487  glbval  15496  joinle  15513  latmlem1  15580  odmulg  16447  efginvrel2  16614  pgpfac1lem5  16998  chfacfscmul0  19226  chfacfpmmul0  19230  1stccnp  19829  qustgplem  20485  imasdsf1olem  20742  bldisj  20767  xbln0  20783  prdsbl  20860  metss2lem  20880  stdbdxmet  20884  ngptgp  21016  nghmcn  21118  icoopnst  21305  iocopnst  21306  cnllycmp  21322  iscau3  21583  cmetcaulem  21593  iscmet3lem1  21596  bcthlem4  21632  ovollb2lem  21765  ovolicc2lem3  21796  voliunlem3  21828  volcn  21881  itg10a  21983  itg1ge0a  21984  dvcnvrelem1  22284  dvfsumrlim  22298  itgsubst  22316  ulmcn  22659  ulmdvlem3  22662  mtest  22664  tanord  22790  emcllem6  23195  ftalem2  23212  chtub  23352  fsumvma2  23354  vmasum  23356  chpchtsum  23359  bcmono  23417  bclbnd  23420  bposlem1  23424  bposlem5  23428  bposlem6  23429  lgsne0  23473  chtppilim  23525  dchrisumlem3  23541  pntrsumbnd2  23617  pntlemf  23655  pntlem3  23659  pntleml  23661  redwlklem  24472  eupath2  24845  grpoidinvlem3  25073  grpoideu  25076  vacn  25469  blocni  25585  ubthlem2  25652  chscllem2  26421  lnconi  26817  pjnmopi  26932  atomli  27166  sumdmdlem2  27203  cdj3lem2b  27221  xraddge02  27442  dfon2lem5  29187  dfon2lem6  29188  cgrcoml  29614  btwnconn2  29720  ltflcei  30011  heicant  30017  mblfinlem3  30021  mblfinlem4  30022  itg2addnclem  30034  itg2addnc  30037  bddiblnc  30053  ftc1anclem6  30063  ftc1anc  30066  mettrifi  30218  geomcau  30220  equivbnd  30254  heibor1lem  30273  bfplem1  30286  bfplem2  30287  rrncmslem  30296  divrngidl  30393  lcmdvdsb  31186  climinf  31516  2ffzoeq  32175  lecmtN  34683  cvrletrN  34700  llnnleat  34939  lplnnle2at  34967  lvolnle3at  35008  dalem21  35120  cdlemblem  35219  osumcllem11N  35392  pexmidlem8N  35403  lhpmcvr4N  35452  cdleme32b  35870  cdleme35fnpq  35877  cdleme48bw  35930  cdlemf1  35989  cdlemg2fv2  36028  cdlemg7fvbwN  36035  cdlemg27b  36124  tendoeq2  36202  dia2dimlem1  36493  dihord6apre  36685  dihord5apre  36691  dihglbcpreN  36729  dochnel2  36821  dihjat1lem  36857  dochexmidlem8  36896  mapdordlem2  37066
  Copyright terms: Public domain W3C validator