Theorem syl6c 71

Description: Inference combining syl6 36 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 36	. 2 ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜏)))
5	1, 4	mpdd 44	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:  syl6ci  72  syldd  73  impbidd  213  pm5.21ndd  382  jcad  521  a2and  858  zorn2lem6  10491  sqreulem  15418  ontopbas  36967  ontgval  36970  ordtoplem  36974  ordcmp  36986  fvineqsneu  38085  jaodd  43005  ee33  45258  sb5ALT  45262  tratrb  45273  onfrALTlem2  45283  onfrALT  45286  ax6e2ndeq  45296  ee22an  45410  sspwtrALT  45558  sspwtrALT2  45559  trintALT  45617