Theorem syl6ci 72

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 26	. 2 ⊢ (𝜑 → (𝜓 → 𝜃))
4		syl6ci.3	. 2 ⊢ (𝜒 → (𝜃 → 𝜏))
5	1, 3, 4	syl6c 71	1 ⊢ (𝜑 → (𝜓 → 𝜏))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  mtord  893  reu6  3687  axprlem3OLD  5398  ordelord  6383  f1dmex  7957  soseq  8160  omeulem2  8573  2pwuninel  9133  isumrpcl  15934  kqfvima  23957  caubl  25537  nbupgr  29790  nbumgrvtx  29792  umgr2adedgspth  30402  btwnconn1lem12  36665  omabs2  44160  sbcim2g  45348  ee21an  45541