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  3731  axprlem3OLD  5427  ordelord  6405  f1dmex  7982  soseq  8185  omeulem2  8622  2pwuninel  9173  isumrpcl  15880  kqfvima  23739  caubl  25343  nbupgr  29362  nbumgrvtx  29364  umgr2adedgspth  29969  btwnconn1lem12  36100  omabs2  43350  sbcim2g  44563  ee21an  44757
  Copyright terms: Public domain W3C validator