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

Theorem mpanl2 679
Description: An inference based on modus ponens. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Andrew Salmon, 7-May-2011.)
Hypotheses
Ref Expression
mpanl2.1  |-  ps
mpanl2.2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
Assertion
Ref Expression
mpanl2  |-  ( (
ph  /\  ch )  ->  th )

Proof of Theorem mpanl2
StepHypRef Expression
1 mpanl2.1 . . 3  |-  ps
21jctr 540 . 2  |-  ( ph  ->  ( ph  /\  ps ) )
3 mpanl2.2 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
42, 3sylan 469 1  |-  ( (
ph  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367
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 369
This theorem is referenced by:  mpanr1  681  mp3an2  1310  reuss  3776  tfrlem11  7049  tfr3  7060  oe0  7164  dif1en  7745  noinfepOLD  8068  indpi  9274  map2psrpr  9476  axcnre  9530  muleqadd  10189  divdiv2  10252  addltmul  10770  frnnn0supp  10845  supxrpnf  11513  supxrunb1  11514  supxrunb2  11515  iimulcl  21606  numclwwlkovf2ex  25291  eigposi  26956  nmopadjlem  27209  nmopcoadji  27221  opsqrlem6  27265  hstrbi  27386  sgncl  28744  aacllem  33623
  Copyright terms: Public domain W3C validator