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

Theorem syl7 70
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 69 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  234  syl3an3  1303  hbae  2149  tz7.7  5449  fvmptt  5965  f1oweALT  6777  wfrlem12  7047  nneneq  7755  pr2nelem  8435  cfcoflem  8702  nnunb  10865  ndvdssub  14388  lsmcv  18364  gsummoncoe1  18898  uvcendim  19405  2ndcsep  20474  atcvat4i  28050  mdsymlem5  28060  sumdmdii  28068  dfon2lem6  30434  frrlem11  30526  colineardim1  30828  bj-hbaeb2  31420  wl-ax12  31913  hbae-o  32473  ax12  32475  cvrat4  33008  llncvrlpln2  33122  lplncvrlvol2  33180  dihmeetlem3N  34873  eel2122old  37103
  Copyright terms: Public domain W3C validator