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  2422  hbae  2430  tz7.7  6339  fvmptt  6963  f1oweALT  7895  wfrlem12OLD  8233  nneneq  9086  nneneqOLD  9098  pr2nelemOLD  9872  cfcoflem  10141  nnunb  12342  ndvdssub  16225  lsmcv  20525  uvcendim  21176  gsummoncoe1  21597  2ndcsep  22732  atcvat4i  31137  mdsymlem5  31147  sumdmdii  31155  dfon2lem6  34153  colineardim1  34541  bj-hbaeb2  35178  hbae-o  37260  ax12fromc15  37262  cvrat4  37801  llncvrlpln2  37915  lplncvrlvol2  37973  dihmeetlem3N  39663  eel2122old  42764
  Copyright terms: Public domain W3C validator