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  210  pm5.21ndd  379  jcad  512  a2and  845  zorn2lem6  10515  sqreulem  15378  ontopbas  36446  ontgval  36449  ordtoplem  36453  ordcmp  36465  fvineqsneu  37429  jaodd  42259  ee33  44546  sb5ALT  44550  tratrb  44561  onfrALTlem2  44571  onfrALT  44574  ax6e2ndeq  44584  ee22an  44698  sspwtrALT  44846  sspwtrALT2  44847  trintALT  44905