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 ⊢ (𝜑 → (𝜓 → 𝜏))

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  72  syldd  73  impbidd  213  pm5.21ndd  382  jcad  521  a2and  858  zorn2lem6  10484  sqreulem  15410  ontopbas  36905  ontgval  36908  ordtoplem  36912  ordcmp  36924  fvineqsneu  38023  jaodd  42945  ee33  45200  sb5ALT  45204  tratrb  45215  onfrALTlem2  45225  onfrALT  45228  ax6e2ndeq  45238  ee22an  45352  sspwtrALT  45500  sspwtrALT2  45501  trintALT  45559