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

Theorem syl6ci 71
Description: A syllogism inference combined with contraction. (Contributed by Alan Sare, 18-Mar-2012.)
Hypotheses
Ref Expression
syl6ci.1 (𝜑 → (𝜓𝜒))
syl6ci.2 (𝜑𝜃)
syl6ci.3 (𝜒 → (𝜃𝜏))
Assertion
Ref Expression
syl6ci (𝜑 → (𝜓𝜏))

Proof of Theorem syl6ci
StepHypRef Expression
1 syl6ci.1 . 2 (𝜑 → (𝜓𝜒))
2 syl6ci.2 . . 3 (𝜑𝜃)
32a1d 25 . 2 (𝜑 → (𝜓𝜃))
4 syl6ci.3 . 2 (𝜒 → (𝜃𝜏))
51, 3, 4syl6c 70 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:  mtord  873  reu6  3714  axprlem3  5316  ordelord  6206  f1dmex  7647  omeulem2  8198  2pwuninel  8660  isumrpcl  15186  kqfvima  22266  caubl  23838  nbupgr  27053  nbumgrvtx  27055  umgr2adedgspth  27654  soseq  32993  btwnconn1lem12  33456  sbcim2g  40749  ee21an  40943
  Copyright terms: Public domain W3C validator