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

Theorem syl56 30
Description: Combine syl5 28 and syl6 29. (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 29 . 2  |-  ( ch 
->  ( ps  ->  ta ) )
51, 4syl5 28 1  |-  ( ch 
->  ( ph  ->  ta ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  spfw  1691  spw  1694  19.8a  1747  dvelimhw  1854  dvelimv  1944  ax10  1949  cbv2h  1985  euind  3028  reuind  3044  tz7.7  4497  cores  5255  tfrlem1  6475  tz7.49  6541  omsmolem  6735  php  7130  hta  7654  carddom2  7697  infdif  7922  isf32lem3  8068  alephval2  8281  cfpwsdom  8293  nqerf  8641  zeo  10186  o1rlimmul  12182  catideu  13670  ufileu  17710  iscau2  18801  scvxcvx  20385  issgon  23772  cvmsss2  24209  onsucconi  25435  onsucsuccmpi  25441  sspwtrALT  28341  dvelimhwNEW7  28861  dvelimvNEW7  28868  ax10NEW7  28879  cbv2hwAUX7  28919  ax7w1AUX7  29045  cbv2hOLD7  29105  ax10lem17ALT  29175  ax10lem18ALT  29176  ax9lem17  29208  lpolsatN  31730  lpolpolsatN  31731
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator