MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl8 Structured version   Visualization version   GIF version

Theorem syl8 76
Description: A syllogism rule of inference. The second premise is used to replace the consequent of the first premise. (Contributed by NM, 1-Aug-1994.) (Proof shortened by Wolf Lammen, 3-Aug-2012.)
Hypotheses
Ref Expression
syl8.1 (𝜑 → (𝜓 → (𝜒𝜃)))
syl8.2 (𝜃𝜏)
Assertion
Ref Expression
syl8 (𝜑 → (𝜓 → (𝜒𝜏)))

Proof of Theorem syl8
StepHypRef Expression
1 syl8.1 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
2 syl8.2 . . 3 (𝜃𝜏)
32a1i 11 . 2 (𝜑 → (𝜃𝜏))
41, 3syl6d 75 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:  a1ddd  80  com45  97  syl8ib  256  mo4  2561  ssorduni  7763  tz7.49  8442  nneneq  9206  nneneqOLD  9218  dfac2b  10122  qreccl  12950  dvdsaddre2b  16247  cmpsub  22896  fclsopni  23511  nocvxminlem  27269  sumdmdlem2  31660  umgr2cycllem  34120  idinside  35045  axc11n11r  35550  isbasisrelowllem1  36225  isbasisrelowllem2  36226  dmqseqim2  37516  disjlem17  37658  prtlem15  37734  prtlem17  37735  ee3bir  43250  ee233  43266  onfrALTlem2  43293  ee223  43381  ee33VD  43626  rngccatidALTV  46841  ringccatidALTV  46904
  Copyright terms: Public domain W3C validator