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

Theorem mpanl2 692
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 549 . 2  |-  ( ph  ->  ( ph  /\  ps ) )
3 mpanl2.2 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
42, 3sylan 478 1  |-  ( (
ph  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375
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 190  df-an 377
This theorem is referenced by:  mpanr1  694  mp3an2  1361  reuss  3735  tfrlem11  7131  tfr3  7142  oe0  7249  dif1en  7829  indpi  9357  map2psrpr  9559  axcnre  9613  muleqadd  10283  divdiv2  10346  addltmul  10876  frnnn0supp  10951  supxrpnf  11632  supxrunb1  11633  supxrunb2  11634  iimulcl  22013  numclwwlkovf2ex  25862  eigposi  27537  nmopadjlem  27790  nmopcoadji  27802  opsqrlem6  27846  hstrbi  27967  sgncl  29457  poimirlem3  31987  aacllem  40812
  Copyright terms: Public domain W3C validator