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  4446  sotri2  5396  ovig  6408  orduniorsuc  6649  omopth2  7233  frfi  7765  ordunifi  7770  finsschain  7827  cantnfp1lem3  8099  cantnfp1  8100  cantnfp1lem3OLD  8125  cantnfp1OLD  8126  p1le  10385  nnge1  10562  zltp1le  10912  gtndiv  10938  uzss  11102  eluzadd  11110  uzm1  11112  xrre2  11371  xrre3  11372  xrmaxlt  11382  xrmaxle  11384  xrsupsslem  11498  xrub  11503  supxrunb1  11511  flflp1  11912  ceile  11944  seqf1olem1  12114  leexp2r  12191  expnlbnd2  12265  facavg  12347  caubnd2  13153  limsupbnd1  13268  limsupbnd2  13269  rlim2lt  13283  rlim3  13284  o1co  13372  mulcn2  13381  cn1lem  13383  rlimo1  13402  climsqz  13426  climsqz2  13427  rlimsqzlem  13434  lo1le  13437  rlimno1  13439  climsup  13455  caucvgrlem2  13460  iseraltlem2  13468  iseralt  13470  fsumabs  13578  cvgcmp  13593  cvgcmpce  13595  isumltss  13623  cvgrat  13655  ruclem9  13832  ruclem12  13835  bitsfzolem  13943  bitsfzo  13944  sadcaddlem  13966  gcdeq  14049  algcvgblem  14065  algcvga  14067  coprm  14100  coprmdvds  14102  eulerthlem2  14171  pclem  14221  infpn2  14290  prmreclem1  14293  prmreclem4  14296  ramtlecl  14377  lubval  15471  lublecllem  15475  glbval  15484  joinle  15501  latmlem1  15568  odmulg  16384  efginvrel2  16551  pgpfac1lem5  16932  chfacfscmul0  19154  chfacfpmmul0  19158  1stccnp  19757  divstgplem  20382  imasdsf1olem  20639  bldisj  20664  xbln0  20680  prdsbl  20757  metss2lem  20777  stdbdxmet  20781  ngptgp  20913  nghmcn  21015  icoopnst  21202  iocopnst  21203  cnllycmp  21219  iscau3  21480  cmetcaulem  21490  iscmet3lem1  21493  bcthlem4  21529  ovollb2lem  21662  ovolicc2lem3  21693  voliunlem3  21725  volcn  21778  itg10a  21880  itg1ge0a  21881  dvcnvrelem1  22181  dvfsumrlim  22195  itgsubst  22213  ulmcn  22556  ulmdvlem3  22559  mtest  22561  tanord  22686  emcllem6  23086  ftalem2  23103  chtub  23243  fsumvma2  23245  vmasum  23247  chpchtsum  23250  bcmono  23308  bclbnd  23311  bposlem1  23315  bposlem5  23319  bposlem6  23320  lgsne0  23364  chtppilim  23416  dchrisumlem3  23432  pntrsumbnd2  23508  pntlemf  23546  pntlem3  23550  pntleml  23552  redwlklem  24311  eupath2  24684  grpoidinvlem3  24912  grpoideu  24915  vacn  25308  blocni  25424  ubthlem2  25491  chscllem2  26260  lnconi  26656  pjnmopi  26771  atomli  27005  sumdmdlem2  27042  cdj3lem2b  27060  xraddge02  27273  dfon2lem5  28824  dfon2lem6  28825  cgrcoml  29251  btwnconn2  29357  ltflcei  29648  heicant  29654  mblfinlem3  29658  mblfinlem4  29659  itg2addnclem  29671  itg2addnc  29674  bddiblnc  29690  ftc1anclem6  29700  ftc1anc  29703  mettrifi  29881  geomcau  29883  equivbnd  29917  heibor1lem  29936  bfplem1  29949  bfplem2  29950  rrncmslem  29959  divrngidl  30056  lcmdvdsb  30845  climinf  31176  2ffzoeq  31836  lecmtN  34071  cvrletrN  34088  llnnleat  34327  lplnnle2at  34355  lvolnle3at  34396  dalem21  34508  cdlemblem  34607  osumcllem11N  34780  pexmidlem8N  34791  lhpmcvr4N  34840  cdleme32b  35256  cdleme35fnpq  35263  cdleme48bw  35316  cdlemf1  35375  cdlemg2fv2  35414  cdlemg7fvbwN  35421  cdlemg27b  35510  tendoeq2  35588  dia2dimlem1  35879  dihord6apre  36071  dihord5apre  36077  dihglbcpreN  36115  dochnel2  36207  dihjat1lem  36243  dochexmidlem8  36282  mapdordlem2  36452
  Copyright terms: Public domain W3C validator