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  877  reu6  3665  axprlem3  5291  ordelord  6181  f1dmex  7640  omeulem2  8192  2pwuninel  8656  isumrpcl  15190  kqfvima  22335  caubl  23912  nbupgr  27134  nbumgrvtx  27136  umgr2adedgspth  27734  soseq  33209  btwnconn1lem12  33672  sbcim2g  41244  ee21an  41438