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  1657  spw  1660  dvelimhw  1735  dvelimv  1879  ax10  1884  cbv2h  1920  euind  2952  reuind  2968  tz7.7  4418  cores  5176  tfrlem1  6391  tz7.49  6457  omsmolem  6651  php  7045  hta  7567  carddom2  7610  infdif  7835  isf32lem3  7981  alephval2  8194  cfpwsdom  8206  nqerf  8554  zeo  10097  o1rlimmul  12092  catideu  13577  ufileu  17614  iscau2  18703  scvxcvx  20280  issgon  23484  cvmsss2  23805  onsucconi  24876  onsucsuccmpi  24882  rngodmeqrn  25419  sspwtrALT  28596  ax10lem17ALT  29123  ax10lem18ALT  29124  ax9lem17  29156  lpolsatN  31678  lpolpolsatN  31679
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator