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

Theorem mpanl2 664
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 528 . 2  |-  ( ph  ->  ( ph  /\  ps ) )
3 mpanl2.2 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
42, 3sylan 459 1  |-  ( (
ph  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360
This theorem is referenced by:  mpanr1  666  mp3an2  1268  reuss  3607  tfrlem11  6678  tfr3  6689  oe0  6795  dif1enOLD  7369  dif1en  7370  noinfepOLD  7644  indpi  8815  map2psrpr  9016  axcnre  9070  muleqadd  9697  divdiv2  9757  addltmul  10234  supxrpnf  10928  supxrunb1  10929  supxrunb2  10930  spwpr4  14694  iimulcl  18993  eigposi  23370  nmopadjlem  23623  nmopcoadji  23635  opsqrlem6  23679  hstrbi  23800  sibfof  24685
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 179  df-an 362
  Copyright terms: Public domain W3C validator