Theorem syl6c 70

Description: Inference combining syl6 35 with contraction. (Contributed by Alan Sare, 2-May-2011.)

Hypotheses

Ref	Expression
syl6c.1	⊢ (𝜑 → (𝜓 → 𝜒))
syl6c.2	⊢ (𝜑 → (𝜓 → 𝜃))
syl6c.3	⊢ (𝜒 → (𝜃 → 𝜏))

Assertion

Ref	Expression
syl6c	⊢ (𝜑 → (𝜓 → 𝜏))

Proof of Theorem syl6c

Step	Hyp	Ref	Expression
1		syl6c.2	. 2 ⊢ (𝜑 → (𝜓 → 𝜃))
2		syl6c.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3		syl6c.3	. . 3 ⊢ (𝜒 → (𝜃 → 𝜏))
4	2, 3	syl6 35	. 2 ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜏)))
5	1, 4	mpdd 43	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:  syl6ci  71  syldd  72  impbidd  209  pm5.21ndd  381  jcad  513  a2and  842  zorn2lem6  10257  sqreulem  15071  ontopbas  34617  ontgval  34620  ordtoplem  34624  ordcmp  34636  fvineqsneu  35582  jaodd  40174  ee33  42141  sb5ALT  42145  tratrb  42156  onfrALTlem2  42166  onfrALT  42169  ax6e2ndeq  42179  ee22an  42293  sspwtrALT  42442  sspwtrALT2  42443  trintALT  42501