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  2036  euind  3085  reuind  3101  tz7.7  4571  cores  5336  tfrlem1  6599  tz7.49  6665  omsmolem  6859  php  7254  hta  7781  carddom2  7824  infdif  8049  isf32lem3  8195  alephval2  8407  cfpwsdom  8419  nqerf  8767  zeo  10315  o1rlimmul  12371  catideu  13859  catpropd  13894  ufileu  17908  iscau2  19187  scvxcvx  20781  issgon  24463  cvmsss2  24918  onsucconi  26095  onsucsuccmpi  26101  sspwtrALT  28648  dvelimhwNEW7  29165  dvelimvNEW7  29172  ax10NEW7  29183  cbv2hwAUX7  29223  ax7w1AUX7  29349  cbv2hOLD7  29409  lpolsatN  31975  lpolpolsatN  31976
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator