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  3683  axprlem3OLD  5364  ordelord  6324  f1dmex  7884  soseq  8084  omeulem2  8493  2pwuninel  9040  isumrpcl  15742  kqfvima  23638  caubl  25228  nbupgr  29315  nbumgrvtx  29317  umgr2adedgspth  29919  btwnconn1lem12  36111  omabs2  43344  sbcim2g  44550  ee21an  44743