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

Theorem syl7 74
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 (𝜑𝜓)
syl7.2 (𝜒 → (𝜃 → (𝜓𝜏)))
Assertion
Ref Expression
syl7 (𝜒 → (𝜃 → (𝜑𝜏)))

Proof of Theorem syl7
StepHypRef Expression
1 syl7.1 . . 3 (𝜑𝜓)
21a1i 11 . 2 (𝜒 → (𝜑𝜓))
3 syl7.2 . 2 (𝜒 → (𝜃 → (𝜓𝜏)))
42, 3syl5d 73 1 (𝜒 → (𝜃 → (𝜑𝜏)))
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  255  ax12  2423  hbae  2431  tz7.7  6340  fvmptt  6964  f1oweALT  7896  wfrlem12OLD  8234  nneneq  9087  nneneqOLD  9099  pr2nelemOLD  9873  cfcoflem  10142  nnunb  12343  ndvdssub  16226  lsmcv  20525  uvcendim  21176  gsummoncoe1  21597  2ndcsep  22732  atcvat4i  31125  mdsymlem5  31135  sumdmdii  31143  dfon2lem6  34141  colineardim1  34532  bj-hbaeb2  35169  hbae-o  37251  ax12fromc15  37253  cvrat4  37792  llncvrlpln2  37906  lplncvrlvol2  37964  dihmeetlem3N  39654  eel2122old  42733
  Copyright terms: Public domain W3C validator