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  354  jcad  533  zorn2lem6  8880  sqreulem  13154  ontopbas  29486  ontgval  29489  ordtoplem  29493  ordcmp  29505  ee33  32379  sb5ALT  32383  tratrb  32395  onfrALTlem2  32407  onfrALT  32410  ax6e2ndeq  32421  ee22an  32548  sspwtrALT  32709  sspwtrALT2  32712  trintALT  32770
  Copyright terms: Public domain W3C validator