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

Theorem syl56 32
Description: Combine syl5 30 and syl6 31. (Contributed by NM, 14-Nov-2013.)
Hypotheses
Ref Expression
syl56.1  |-  ( ph  ->  ps )
syl56.2  |-  ( ch 
->  ( ps  ->  th )
)
syl56.3  |-  ( th 
->  ta )
Assertion
Ref Expression
syl56  |-  ( ch 
->  ( ph  ->  ta ) )

Proof of Theorem syl56
StepHypRef Expression
1 syl56.1 . 2  |-  ( ph  ->  ps )
2 syl56.2 . . 3  |-  ( ch 
->  ( ps  ->  th )
)
3 syl56.3 . . 3  |-  ( th 
->  ta )
42, 3syl6 31 . 2  |-  ( ch 
->  ( ps  ->  ta ) )
51, 4syl5 30 1  |-  ( ch 
->  ( ph  ->  ta ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  spfw  1699  spwOLD  1703  19.8a  1758  dvelimhwOLD  1873  dvelimvOLD  1994  ax10OLD  1998  cbv2h  2033  euind  3081  reuind  3097  tz7.7  4567  cores  5332  tfrlem1  6595  tz7.49  6661  omsmolem  6855  php  7250  hta  7777  carddom2  7820  infdif  8045  isf32lem3  8191  alephval2  8403  cfpwsdom  8415  nqerf  8763  zeo  10311  o1rlimmul  12367  catideu  13855  catpropd  13890  ufileu  17904  iscau2  19183  scvxcvx  20777  issgon  24459  cvmsss2  24914  onsucconi  26091  onsucsuccmpi  26097  sspwtrALT  28644  dvelimhwNEW7  29161  dvelimvNEW7  29168  ax10NEW7  29179  cbv2hwAUX7  29219  ax7w1AUX7  29345  cbv2hOLD7  29405  lpolsatN  31971  lpolpolsatN  31972
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator