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

Theorem syl6ci 69
 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 68 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:  ordelord  5662  f1dmex  7029  omeulem2  7550  2pwuninel  8000  isumrpcl  14414  kqfvima  21343  caubl  22914  frgrawopreglem2  26572  soseq  30995  btwnconn1lem12  31375  sbcim2g  37769  ee21an  37980  nbupgr  40566  nbumgrvtx  40568  umgr2adedgspth  41155
 Copyright terms: Public domain W3C validator