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  879  reu6  3735  axprlem3OLD  5434  ordelord  6408  f1dmex  7980  soseq  8183  omeulem2  8620  2pwuninel  9171  isumrpcl  15876  kqfvima  23754  caubl  25356  nbupgr  29376  nbumgrvtx  29378  umgr2adedgspth  29978  btwnconn1lem12  36080  omabs2  43322  sbcim2g  44536  ee21an  44730
  Copyright terms: Public domain W3C validator