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  245  syl3an3  1498  ax12  2437  hbae  2445  ax12OLD  2469  tz7.7  5898  fvmptt  6450  f1oweALT  7305  wfrlem12  7583  nneneq  8296  pr2nelem  8988  cfcoflem  9257  nnunb  11451  ndvdssub  15306  lsmcv  19314  gsummoncoe1  19847  uvcendim  20359  2ndcsep  21435  atcvat4i  29536  mdsymlem5  29546  sumdmdii  29554  dfon2lem6  31969  colineardim1  32445  bj-hbaeb2  33082  hbae-o  34661  ax12fromc15  34663  cvrat4  35201  llncvrlpln2  35315  lplncvrlvol2  35373  dihmeetlem3N  37065  eel2122old  39414
 Copyright terms: Public domain W3C validator