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  369  jcad  555  zorn2lem6  9267  sqreulem  14033  ontopbas  32069  ontgval  32072  ordtoplem  32076  ordcmp  32088  ee33  38209  sb5ALT  38213  tratrb  38228  onfrALTlem2  38243  onfrALT  38246  ax6e2ndeq  38257  ee22an  38380  sspwtrALT  38532  sspwtrALT2  38541  trintALT  38600
  Copyright terms: Public domain W3C validator