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

Theorem syl7 65
Description: A syllogism rule of inference. The first premise is used to replace the third antecedent of the second premise. (Contributed by NM, 5-Aug-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 64 1  |-  ( ch 
->  ( th  ->  ( ph  ->  ta ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  syl7bi  222  syl3an3  1219  ax10lem4OLD  2030  hbae  2040  hbaeOLD  2041  hbae-o  2230  ax11  2232  tz7.7  4607  fvmptt  5820  f1oweALT  6074  nneneq  7290  pr2nelem  7888  cfcoflem  8152  nnunb  10217  ndvdssub  12927  lsmcv  16213  2ndcsep  17522  atcvat4i  23900  mdsymlem5  23910  sumdmdii  23918  dfon2lem6  25415  wfrlem12  25549  frrlem11  25594  colineardim1  25995  eel2122old  28828  ax10lem4NEW7  29471  hbaewAUX7  29478  hbaew0AUX7  29647  hbaeOLD7  29708  cvrat4  30240  llncvrlpln2  30354  lplncvrlvol2  30412  dihmeetlem3N  32103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator