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

Theorem syl7 70
Description: A syllogism rule of inference. The first premise is used to replace the third antecedent of the second premise. (Contributed by NM, 12-Jan-1993.) (Proof shortened by Wolf Lammen, 3-Aug-2012.)
Hypotheses
Ref Expression
syl7.1  |-  ( ph  ->  ps )
syl7.2  |-  ( ch 
->  ( th  ->  ( ps  ->  ta ) ) )
Assertion
Ref Expression
syl7  |-  ( ch 
->  ( th  ->  ( ph  ->  ta ) ) )

Proof of Theorem syl7
StepHypRef Expression
1 syl7.1 . . 3  |-  ( ph  ->  ps )
21a1i 11 . 2  |-  ( ch 
->  ( ph  ->  ps ) )
3 syl7.2 . 2  |-  ( ch 
->  ( th  ->  ( ps  ->  ta ) ) )
42, 3syl5d 69 1  |-  ( ch 
->  ( th  ->  ( ph  ->  ta ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  syl7bi  233  syl3an3  1299  hbae  2110  tz7.7  5464  fvmptt  5977  f1oweALT  6787  wfrlem12  7051  nneneq  7757  pr2nelem  8436  cfcoflem  8702  nnunb  10865  ndvdssub  14375  lsmcv  18351  gsummoncoe1  18885  uvcendim  19391  2ndcsep  20460  atcvat4i  28035  mdsymlem5  28045  sumdmdii  28053  dfon2lem6  30428  frrlem11  30520  colineardim1  30820  bj-hbaeb2  31377  wl-ax12  31826  hbae-o  32391  ax12  32393  cvrat4  32926  llncvrlpln2  33040  lplncvrlvol2  33098  dihmeetlem3N  34791  eel2122old  36963
  Copyright terms: Public domain W3C validator