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  522  a2and  859  zorn2lem6  10579  sqreulem  15527  ontopbas  37258  ontgval  37261  ordtoplem  37265  ordcmp  37277  fvineqsneu  38377  jaodd  43303  ee33  45547  sb5ALT  45551  tratrb  45562  onfrALTlem2  45572  onfrALT  45575  ax6e2ndeq  45585  ee22an  45699  sspwtrALT  45847  sspwtrALT2  45848  trintALT  45906