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

Theorem mpanl2 662
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 526 . 2  |-  ( ph  ->  ( ph  /\  ps ) )
3 mpanl2.2 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
42, 3sylan 457 1  |-  ( (
ph  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  mpanr1  664  mp3an2  1265  reuss  3462  tfrlem11  6420  tfr3  6431  oe0  6537  dif1enOLD  7106  dif1en  7107  noinfepOLD  7377  indpi  8547  map2psrpr  8748  axcnre  8802  muleqadd  9428  divdiv2  9488  addltmul  9963  supxrpnf  10653  supxrunb1  10654  supxrunb2  10655  spwpr4  14356  iimulcl  18451  eigposi  22432  nmopadjlem  22685  nmopcoadji  22697  opsqrlem6  22741  hstrbi  22862
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator