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  254  ax12  2417  hbae  2425  ceqsalt  3496  elabgt  3658  tz7.7  6394  fvmptt  7021  f1oweALT  7978  wfrlem12OLD  8342  nneneq  9236  nneneqOLD  9248  pr2nelemOLD  10039  cfcoflem  10306  nnunb  12514  ndvdssub  16406  lsmcv  21118  uvcendim  21841  gsummoncoe1  22296  2ndcsep  23451  atcvat4i  32327  mdsymlem5  32337  sumdmdii  32345  dfon2lem6  35625  colineardim1  35898  bj-hbaeb2  36536  hbae-o  38614  ax12fromc15  38616  cvrat4  39155  llncvrlpln2  39269  lplncvrlvol2  39327  dihmeetlem3N  41017  naddgeoa  43098  eel2122old  44431
  Copyright terms: Public domain W3C validator