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  213  pm5.21ndd  384  jcad  516  a2and  842  zorn2lem6  9912  sqreulem  14711  ontopbas  33889  ontgval  33892  ordtoplem  33896  ordcmp  33908  fvineqsneu  34828  jaodd  39390  ee33  41227  sb5ALT  41231  tratrb  41242  onfrALTlem2  41252  onfrALT  41255  ax6e2ndeq  41265  ee22an  41379  sspwtrALT  41528  sspwtrALT2  41529  trintALT  41587