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  1263  hbae  2056  equveliOLD  2090  hbae-o  2233  ax12  2235  tz7.7  4913  fvmptt  5972  f1oweALT  6783  nneneq  7719  pr2nelem  8399  cfcoflem  8669  nnunb  10812  ndvdssub  14077  lsmcv  17914  gsummoncoe1  18473  uvcendim  19009  2ndcsep  20086  atcvat4i  27443  mdsymlem5  27453  sumdmdii  27461  dfon2lem6  29437  wfrlem12  29571  frrlem11  29616  colineardim1  29916  eel2122old  33656  bj-hbaeb2  34534  cvrat4  35310  llncvrlpln2  35424  lplncvrlvol2  35482  dihmeetlem3N  37175
  Copyright terms: Public domain W3C validator