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

Theorem syl7 63
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 10 . 2  |-  ( ch 
->  ( ph  ->  ps ) )
3 syl7.2 . 2  |-  ( ch 
->  ( th  ->  ( ps  ->  ta ) ) )
42, 3syl5d 62 1  |-  ( ch 
->  ( th  ->  ( ph  ->  ta ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  syl7bi  221  syl3an3  1217  ax10lem4  1894  hbae  1906  hbae-o  2105  ax11  2107  tz7.7  4434  fvmptt  5631  f1oweALT  5867  nneneq  7060  pr2nelem  7650  cfcoflem  7914  nnunb  9977  ndvdssub  12622  lsmcv  15910  2ndcsep  17201  atcvat4i  22993  mdsymlem5  23003  sumdmdii  23011  dfon2lem6  24215  wfrlem12  24338  frrlem11  24364  colineardim1  24756  lvsovso  25729  icmpmon  25919  eel2122old  28805  ax10lem4NEW7  29448  hbaewAUX7  29455  hbaew0AUX7  29617  hbaeOLD7  29662  ax10lem18ALT  29746  a12study  29754  a12study3  29757  cvrat4  30254  llncvrlpln2  30368  lplncvrlvol2  30426  dihmeetlem3N  32117
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator