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  245  syl3an3  1358  ax12  2303  hbae  2314  ax12OLD  2340  tz7.7  5718  fvmptt  6266  f1oweALT  7112  wfrlem12  7386  nneneq  8103  pr2nelem  8787  cfcoflem  9054  nnunb  11248  ndvdssub  15076  lsmcv  19081  gsummoncoe1  19614  uvcendim  20126  2ndcsep  21202  atcvat4i  29144  mdsymlem5  29154  sumdmdii  29162  dfon2lem6  31447  frrlem11  31546  colineardim1  31863  bj-hbaeb2  32501  hbae-o  33707  ax12fromc15  33709  cvrat4  34248  llncvrlpln2  34362  lplncvrlvol2  34420  dihmeetlem3N  36113  eel2122old  38464
  Copyright terms: Public domain W3C validator