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  212  pm5.21ndd  381  jcad  520  a2and  856  zorn2lem6  10469  sqreulem  15397  ontopbas  36793  ontgval  36796  ordtoplem  36800  ordcmp  36812  fvineqsneu  37910  jaodd  42830  ee33  45088  sb5ALT  45092  tratrb  45103  onfrALTlem2  45113  onfrALT  45116  ax6e2ndeq  45126  ee22an  45240  sspwtrALT  45388  sspwtrALT2  45389  trintALT  45447