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

Step	Hyp	Ref	Expression
1		syl6ci.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		syl6ci.2	. . 3 ⊢ (𝜑 → 𝜃)
3	2	a1d 25	. 2 ⊢ (𝜑 → (𝜓 → 𝜃))
4		syl6ci.3	. 2 ⊢ (𝜒 → (𝜃 → 𝜏))
5	1, 3, 4	syl6c 70	1 ⊢ (𝜑 → (𝜓 → 𝜏))

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  880  reu6  3685  axprlem3OLD  5374  ordelord  6340  f1dmex  7903  soseq  8103  omeulem2  8512  2pwuninel  9064  isumrpcl  15770  kqfvima  23678  caubl  25268  nbupgr  29400  nbumgrvtx  29402  umgr2adedgspth  30004  btwnconn1lem12  36273  omabs2  43610  sbcim2g  44815  ee21an  45008