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  556  zorn2lem6  9536  sqreulem  14319  ontopbas  32755  ontgval  32758  ordtoplem  32762  ordcmp  32774  ee33  39248  sb5ALT  39252  tratrb  39267  onfrALTlem2  39282  onfrALT  39285  ax6e2ndeq  39296  ee22an  39419  sspwtrALT  39570  sspwtrALT2  39576  trintALT  39635
 Copyright terms: Public domain W3C validator