MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl6c Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 syl6c.2 . 2 (𝜑 → (𝜓𝜃))
2 syl6c.1 . . 3 (𝜑 → (𝜓𝜒))
3 syl6c.3 . . 3 (𝜒 → (𝜃𝜏))
42, 3syl6 35 . 2 (𝜑 → (𝜓 → (𝜃𝜏)))
51, 4mpdd 43 1 (𝜑 → (𝜓𝜏))
Colors of variables: wff setvar class
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  200  pm5.21ndd  368  jcad  502  zorn2lem6  9523  sqreulem  14300  ontopbas  32757  ontgval  32760  ordtoplem  32764  ordcmp  32776  jaodd  37766  ee33  39245  sb5ALT  39249  tratrb  39264  onfrALTlem2  39279  onfrALT  39282  ax6e2ndeq  39293  ee22an  39416  sspwtrALT  39567  sspwtrALT2  39573  trintALT  39632
  Copyright terms: Public domain W3C validator