Theorem syl6c 68

Description: Inference combining syl6 34 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 34	. 2 ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜏)))
5	1, 4	mpdd 42	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  69  syldd  70  impbidd  199  pm5.21ndd  368  jcad  554  zorn2lem6  9206  sqreulem  13947  ontopbas  31597  ontgval  31600  ordtoplem  31604  ordcmp  31616  ee33  37748  sb5ALT  37752  tratrb  37767  onfrALTlem2  37782  onfrALT  37785  ax6e2ndeq  37796  ee22an  37919  sspwtrALT  38071  sspwtrALT2  38080  trintALT  38139