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  258  ax12  2437  hbae  2445  tz7.7  6189  fvmptt  6769  f1oweALT  7659  wfrlem12  7953  nneneq  8688  pr2nelem  9419  cfcoflem  9687  nnunb  11885  ndvdssub  15753  lsmcv  19909  uvcendim  20539  gsummoncoe1  20936  2ndcsep  22067  atcvat4i  30183  mdsymlem5  30193  sumdmdii  30201  dfon2lem6  33141  colineardim1  33630  bj-hbaeb2  34251  hbae-o  36192  ax12fromc15  36194  cvrat4  36732  llncvrlpln2  36846  lplncvrlvol2  36904  dihmeetlem3N  38594  eel2122old  41411
  Copyright terms: Public domain W3C validator