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

Theorem syl6c 64
Description: Inference combining syl6 33 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 33 . 2  |-  ( ph  ->  ( ps  ->  ( th  ->  ta ) ) )
51, 4mpdd 40 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  65  syldd  66  impbidd  189  pm5.21ndd  352  jcad  531  zorn2lem6  8794  sqreulem  13194  ontopbas  30046  ontgval  30049  ordtoplem  30053  ordcmp  30065  ee33  33624  sb5ALT  33628  tratrb  33643  onfrALTlem2  33658  onfrALT  33661  ax6e2ndeq  33672  ee22an  33799  sspwtrALT  33960  sspwtrALT2  33969  trintALT  34028
  Copyright terms: Public domain W3C validator