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

Theorem syl56 33
Description: Combine syl5 31 and syl6 32. (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 32 . 2  |-  ( ch 
->  ( ps  ->  ta ) )
51, 4syl5 31 1  |-  ( ch 
->  ( ph  ->  ta ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  spfw  1704  spwOLD  1708  19.8a  1763  dvelimhwOLD  1878  cbv2h  1980  dvelimvOLD  2029  ax10OLD  2033  exdistrf  2067  euind  3123  reuind  3139  tz7.7  4610  cores  5376  tfrlem1  6639  tz7.49  6705  omsmolem  6899  php  7294  hta  7826  carddom2  7869  infdif  8094  isf32lem3  8240  alephval2  8452  cfpwsdom  8464  nqerf  8812  zeo  10360  o1rlimmul  12417  catideu  13905  catpropd  13940  ufileu  17956  iscau2  19235  scvxcvx  20829  issgon  24511  cvmsss2  24966  onsucconi  26192  onsucsuccmpi  26198  sspwtrALT  29009  dvelimhwNEW7  29529  dvelimvNEW7  29536  ax10NEW7  29547  cbv2hwAUX7  29587  ax7w1AUX7  29719  cbv2hOLD7  29795  lpolsatN  32360  lpolpolsatN  32361
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
  Copyright terms: Public domain W3C validator