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

Theorem mpanl2 681
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 542 . 2  |-  ( ph  ->  ( ph  /\  ps ) )
3 mpanl2.2 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
42, 3sylan 471 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:  mpanr1  683  mp3an2  1313  reuss  3764  tfrlem11  7059  tfr3  7070  oe0  7174  dif1enOLD  7754  dif1en  7755  noinfepOLD  8080  indpi  9288  map2psrpr  9490  axcnre  9544  muleqadd  10199  divdiv2  10262  addltmul  10780  frnnn0supp  10855  supxrpnf  11519  supxrunb1  11520  supxrunb2  11521  iimulcl  21310  numclwwlkovf2ex  24958  eigposi  26627  nmopadjlem  26880  nmopcoadji  26892  opsqrlem6  26936  hstrbi  27057  sgncl  28350
  Copyright terms: Public domain W3C validator