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

Theorem syl7 68
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 67 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  230  syl3an3  1254  hbae  2015  equveliOLD  2049  hbae-o  2212  ax12  2214  tz7.7  4856  fvmptt  5901  f1oweALT  6674  nneneq  7607  pr2nelem  8285  cfcoflem  8555  nnunb  10689  ndvdssub  13732  lsmcv  17348  uvcendim  18404  2ndcsep  19198  atcvat4i  25973  mdsymlem5  25983  sumdmdii  25991  dfon2lem6  27765  wfrlem12  27899  frrlem11  27944  colineardim1  28256  gsummoncoe1  31016  eel2122old  31801  cvrat4  33445  llncvrlpln2  33559  lplncvrlvol2  33617  dihmeetlem3N  35308
  Copyright terms: Public domain W3C validator