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  247  ax12  2357  hbae  2365  tz7.7  6049  fvmptt  6608  f1oweALT  7478  wfrlem12  7763  nneneq  8488  pr2nelem  9216  cfcoflem  9484  nnunb  11696  ndvdssub  15610  lsmcv  19625  gsummoncoe1  20165  uvcendim  20683  2ndcsep  21761  atcvat4i  29945  mdsymlem5  29955  sumdmdii  29963  dfon2lem6  32493  colineardim1  32983  bj-hbaeb2  33572  hbae-o  35432  ax12fromc15  35434  cvrat4  35972  llncvrlpln2  36086  lplncvrlvol2  36144  dihmeetlem3N  37834  eel2122old  40415
  Copyright terms: Public domain W3C validator