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  879  reu6  3688  axprlem3OLD  5370  ordelord  6333  f1dmex  7899  soseq  8099  omeulem2  8508  2pwuninel  9056  isumrpcl  15768  kqfvima  23633  caubl  25224  nbupgr  29307  nbumgrvtx  29309  umgr2adedgspth  29911  btwnconn1lem12  36071  omabs2  43305  sbcim2g  44512  ee21an  44705