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  2428  hbae  2436  ceqsalt  3515  elabgt  3672  tz7.7  6410  fvmptt  7036  f1oweALT  7997  wfrlem12OLD  8360  nneneq  9246  nneneqOLD  9258  pr2nelemOLD  10043  cfcoflem  10312  nnunb  12522  ndvdssub  16446  lsmcv  21143  uvcendim  21867  gsummoncoe1  22312  2ndcsep  23467  atcvat4i  32416  mdsymlem5  32426  sumdmdii  32434  dfon2lem6  35789  colineardim1  36062  bj-hbaeb2  36819  hbae-o  38904  ax12fromc15  38906  cvrat4  39445  llncvrlpln2  39559  lplncvrlvol2  39617  dihmeetlem3N  41307  naddgeoa  43407  eel2122old  44738
  Copyright terms: Public domain W3C validator