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  878  reu6  3684  axprlem3  5380  ordelord  6339  f1dmex  7888  soseq  8090  omeulem2  8529  2pwuninel  9075  isumrpcl  15727  kqfvima  23079  caubl  24670  nbupgr  28290  nbumgrvtx  28292  umgr2adedgspth  28891  btwnconn1lem12  34674  omabs2  41643  sbcim2g  42802  ee21an  42996
  Copyright terms: Public domain W3C validator