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

Theorem syl6c 66
Description: Inference combining syl6 34 with contraction. (Contributed by Alan Sare, 2-May-2011.)
Hypotheses
Ref Expression
syl6c.1  |-  ( ph  ->  ( ps  ->  ch ) )
syl6c.2  |-  ( ph  ->  ( ps  ->  th )
)
syl6c.3  |-  ( ch 
->  ( th  ->  ta ) )
Assertion
Ref Expression
syl6c  |-  ( ph  ->  ( ps  ->  ta ) )

Proof of Theorem syl6c
StepHypRef Expression
1 syl6c.2 . 2  |-  ( ph  ->  ( ps  ->  th )
)
2 syl6c.1 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
3 syl6c.3 . . 3  |-  ( ch 
->  ( th  ->  ta ) )
42, 3syl6 34 . 2  |-  ( ph  ->  ( ps  ->  ( th  ->  ta ) ) )
51, 4mpdd 41 1  |-  ( ph  ->  ( ps  ->  ta ) )
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  67  syldd  68  impbidd  191  pm5.21ndd  355  jcad  535  zorn2lem6  8938  sqreulem  13422  ontopbas  31093  ontgval  31096  ordtoplem  31100  ordcmp  31112  ee33  36848  sb5ALT  36852  tratrb  36867  onfrALTlem2  36882  onfrALT  36885  ax6e2ndeq  36896  ee22an  37023  sspwtrALT  37183  sspwtrALT2  37192  trintALT  37251
  Copyright terms: Public domain W3C validator