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  2028  equveliOLD  2062  hbae-o  2225  ax12  2227  tz7.7  4904  fvmptt  5966  f1oweALT  6769  nneneq  7701  pr2nelem  8383  cfcoflem  8653  nnunb  10792  ndvdssub  13927  lsmcv  17599  gsummoncoe1  18157  uvcendim  18689  2ndcsep  19766  atcvat4i  27089  mdsymlem5  27099  sumdmdii  27107  dfon2lem6  29073  wfrlem12  29207  frrlem11  29252  colineardim1  29564  eel2122old  32810  bj-hbaeb2  33689  cvrat4  34456  llncvrlpln2  34570  lplncvrlvol2  34628  dihmeetlem3N  36319
  Copyright terms: Public domain W3C validator