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  246  syl3an3OLD  1206  ax12  2404  hbae  2411  tz7.7  5934  fvmptt  6489  f1oweALT  7350  wfrlem12  7630  nneneq  8350  pr2nelem  9078  cfcoflem  9347  nnunb  11534  ndvdssub  15416  lsmcv  19414  gsummoncoe1  19947  uvcendim  20462  2ndcsep  21542  atcvat4i  29647  mdsymlem5  29657  sumdmdii  29665  dfon2lem6  32068  colineardim1  32544  bj-hbaeb2  33166  hbae-o  34791  ax12fromc15  34793  cvrat4  35331  llncvrlpln2  35445  lplncvrlvol2  35503  dihmeetlem3N  37193  eel2122old  39537
  Copyright terms: Public domain W3C validator