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  ceqsalt  3506  tz7.7  6391  fvmptt  7019  f1oweALT  7959  wfrlem12OLD  8320  nneneq  9209  nneneqOLD  9221  pr2nelemOLD  9998  cfcoflem  10267  nnunb  12468  ndvdssub  16352  lsmcv  20754  uvcendim  21402  gsummoncoe1  21828  2ndcsep  22963  atcvat4i  31650  mdsymlem5  31660  sumdmdii  31668  dfon2lem6  34760  colineardim1  35033  bj-hbaeb2  35696  hbae-o  37773  ax12fromc15  37775  cvrat4  38314  llncvrlpln2  38428  lplncvrlvol2  38486  dihmeetlem3N  40176  naddgeoa  42145  eel2122old  43479
  Copyright terms: Public domain W3C validator