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  3449  tfrlem11  6404  tfr3  6415  oe0  6521  dif1enOLD  7090  dif1en  7091  noinfepOLD  7361  indpi  8531  map2psrpr  8732  axcnre  8786  muleqadd  9412  divdiv2  9472  addltmul  9947  supxrpnf  10637  supxrunb1  10638  supxrunb2  10639  spwpr4  14340  iimulcl  18435  eigposi  22416  nmopadjlem  22669  nmopcoadji  22681  opsqrlem6  22725  hstrbi  22846
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