MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl6ss Structured version   Visualization version   GIF version

Theorem syl6ss 3579
Description: Subclass transitivity deduction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
Hypotheses
Ref Expression
syl6ss.1 (𝜑𝐴𝐵)
syl6ss.2 𝐵𝐶
Assertion
Ref Expression
syl6ss (𝜑𝐴𝐶)

Proof of Theorem syl6ss
StepHypRef Expression
1 syl6ss.1 . 2 (𝜑𝐴𝐵)
2 syl6ss.2 . . 3 𝐵𝐶
32a1i 11 . 2 (𝜑𝐵𝐶)
41, 3sstrd 3577 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3539
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-in 3546  df-ss 3553
This theorem is referenced by:  difss2  3700  rintn0  4546  eqbrrdva  5201  ssxpb  5473  relfld  5564  funssxp  5960  dff2  6264  dff3  6265  fliftf  6443  1stcof  7065  2ndcof  7066  nnunifi  8074  elfiun  8197  marypha1lem  8200  marypha1  8201  ordtypelem7  8290  tcmin  8478  unwf  8534  rankfu  8601  tcrank  8608  aceq3lem  8804  dfac12lem2  8827  ackbij1lem9  8911  ackbij1lem10  8912  ackbij1lem16  8918  fin23lem26  9008  fin23lem27  9011  fin1a2lem6  9088  itunitc  9104  axdc3lem2  9134  ttukeylem5  9196  fpwwe2lem13  9321  canthwelem  9329  pwfseqlem4  9341  wunex2  9417  wunex3  9420  inar1  9454  inatsk  9457  gruina  9497  suprfinzcl  11327  suprzub  11614  uzsupss  11615  uzwo3  11618  rpnnen1lem4  11652  rpnnen1lem5  11653  rpnnen1lem4OLD  11658  rpnnen1lem5OLD  11659  supxrre  11988  infxrre  11997  ioodisj  12132  supicclub2  12153  fzssnn  12214  fzossnn0  12326  elfzom1elp1fzo  12360  injresinjlem  12408  uzindi  12601  ssnn0fi  12604  seqcoll  13060  seqcoll2  13061  reltrclfv  13555  relexpdmg  13579  relexpdm  13580  relexprng  13583  relexprn  13584  relexpfld  13586  relexpaddg  13590  limsupval2  14008  limsupgre  14009  limsupbnd2  14011  rlimuni  14078  rlimcld2  14106  rlimno1  14181  isercolllem2  14193  isercoll  14195  summolem2a  14242  summolem2  14243  fsumsers  14255  fsumcvg3  14256  prodmolem2a  14452  prodmolem2  14453  zprod  14455  lcmfnnval  15124  lcmfnncl  15129  4sqlem11  15446  vdwlem8  15479  vdwlem11  15482  ramub2  15505  0ram  15511  0ram2  15512  0ramcl  15514  ramub1lem2  15518  prmgaplem3  15544  prmgaplem4  15545  isohom  16208  funcres2c  16333  resscntz  17536  cntzidss  17542  cntzmhm2  17544  pgpssslw  17801  cntzspan  18019  gsumval3  18080  gsum2d  18143  dprdspan  18198  dprdres  18199  lssintcl  18734  lbsextlem2  18929  lbsextlem3  18930  lbsextlem4  18931  mplbas2  19240  islinds3  19940  fctop  20566  cctop  20568  neitr  20742  ordtbas2  20753  ordtopn1  20756  ordtopn2  20757  lmss  20860  clscon  20991  2ndcdisj  21017  2ndcomap  21019  ptbasfi  21142  txcmplem2  21203  hausdiag  21206  txkgen  21213  basqtop  21272  alexsubb  21608  alexsubALTlem4  21612  tsmsres  21705  tsmsxplem1  21714  tsmsxp  21716  ustrel  21773  utop3cls  21813  prdsmet  21933  metustrel  22115  icccmplem2  22382  xrge0tsms  22393  cnmptre  22482  icchmeo  22496  bndth  22513  lebnumlem2  22517  cfilresi  22846  causs  22849  bcthlem5  22878  evthicc  22980  ovolficcss  22990  ovolmge0  22997  ovolgelb  23000  ovollb2lem  23008  ovollb2  23009  ovolunlem1a  23016  ovolunlem1  23017  ovoliunlem1  23022  ovoliunlem2  23023  ovoliun  23025  ovolscalem1  23033  ovolicc1  23036  ovolicc2lem4  23040  ovolicc2  23042  voliunlem2  23071  voliunlem3  23072  ioombl1lem2  23079  ioombl1lem4  23081  uniioovol  23098  uniiccvol  23099  uniioombllem1  23100  uniioombllem2  23102  uniioombllem3  23104  uniioombllem4  23105  uniioombllem6  23107  dyadmbllem  23118  dyadmbl  23119  volcn  23125  vitalilem4  23131  vitalilem5  23132  cnmbf  23177  i1fmul  23214  itg1addlem4  23217  itg2seq  23260  dvbssntr  23415  dvreslem  23424  dvcjbr  23463  dvferm1  23497  dvferm2  23499  cmvth  23503  dvlip  23505  lhop1lem  23525  lhop2  23527  lhop  23528  dvcnvrelem2  23530  dvcnvre  23531  dvfsumle  23533  dvfsumge  23534  dvfsumabs  23535  dvfsumlem2  23539  ftc1a  23549  ftc1lem3  23550  ftc1lem6  23553  itgsubstlem  23560  mdegleb  23573  mdeglt  23574  mdegldg  23575  mdegxrcl  23576  mdegcl  23578  deg1mul3le  23625  ig1pdvds  23685  plyeq0lem  23715  aannenlem2  23833  aalioulem3  23838  taylf  23864  taylthlem2  23877  pserulm  23925  psercn2  23926  psercn  23929  reeff1olem  23949  efcvx  23952  loglesqrt  24244  rlimcnp  24437  xrlimcnp  24440  jensen  24460  wilthlem2  24540  vmadivsumb  24917  pntrsumo1  24999  pntlem3  25043  perpln2  25352  axcontlem10  25599  usgraexmplef  25723  nmoxr  26839  nmooge0  26840  nmoolb  26844  nmoubi  26845  ubthlem1  26944  shmodi  27467  nmopxr  27943  nmfnxr  27956  nmoplb  27984  nmopub  27985  nmfnlb  28001  nmfnleub  28002  nmopun  28091  branmfn  28182  mdslj1i  28396  hatomistici  28439  xppreima2  28664  fpwrelmap  28730  infxrge0gelb  28755  xrge0tsmsd  28950  metideq  29098  metider  29099  pstmfval  29101  esumgect  29313  esum2d  29316  sigaclci  29356  insiga  29361  omssubadd  29523  eulerpartlemgs2  29603  ballotlemsima  29738  signsply0  29788  bnj1145  30149  bnj1137  30151  bnj1136  30153  rescon  30316  cvmliftlem8  30362  cvmlift3lem6  30394  mclsssvlem  30547  mclsind  30555  mclsppslem  30568  nofulllem5  30939  ivthALT  31334  neibastop1  31358  topjoin  31364  ptrecube  32403  poimirlem6  32409  poimirlem15  32418  heicant  32438  mblfinlem2  32441  mblfinlem3  32442  mblfinlem4  32443  ismblfin  32444  itg2gt0cn  32459  ftc1cnnc  32478  ftc1anclem3  32481  ftc1anclem7  32485  ftc1anclem8  32486  ftc1anc  32487  areacirclem2  32495  areacirclem3  32496  areacirclem4  32497  totbndbnd  32582  prdsbnd  32586  heiborlem1  32604  rrnequiv  32628  reheibor  32632  iccbnd  32633  pmapssbaN  33888  2polssN  34043  paddunN  34055  poldmj1N  34056  ispsubcl2N  34075  psubclinN  34076  paddatclN  34077  poml4N  34081  diaglbN  35186  diaintclN  35189  dibglbN  35297  dibintclN  35298  dicssdvh  35317  dihvalrel  35410  dochexmidlem4  35594  rmxyelqirr  36317  ttac  36445  hbtlem6  36542  hbt  36543  itgpowd  36643  cnvssb  36735  cnvrcl0  36775  cnvtrrel  36805  relexpaddss  36853  cotrcltrcl  36860  cotrclrcl  36877  frege96d  36884  frege97d  36887  frege109d  36892  frege131d  36899  rp-imass  36909  rfovcnvf1od  37142  isotone2  37191  gneispace  37276  k0004ss1  37293  uzfissfz  38307  suplesup  38320  limciccioolb  38512  limcicciooub  38528  limcleqr  38535  cncfiooicclem1  38603  ibliccsinexp  38666  iblioosinexp  38668  itgcoscmulx  38685  itgsincmulx  38690  itgsubsticclem  38691  itgiccshift  38696  itgperiod  38697  itgsbtaddcnst  38698  stoweidlem34  38751  stoweidlem59  38776  dirkeritg  38819  dirkercncflem2  38821  fourierdlem20  38844  fourierdlem31  38855  fourierdlem39  38863  fourierdlem42  38866  fourierdlem46  38869  fourierdlem52  38875  fourierdlem53  38876  fourierdlem60  38883  fourierdlem61  38884  fourierdlem62  38885  fourierdlem68  38891  fourierdlem76  38899  fourierdlem85  38908  fourierdlem88  38911  fourierdlem89  38912  fourierdlem90  38913  fourierdlem91  38914  fourierdlem93  38916  fourierdlem94  38917  fourierdlem103  38926  fourierdlem104  38927  fourierdlem111  38934  fouriersw  38948  etransclem46  38997  etransclem48  38999  sge0less  39109  sge0resplit  39123  sge0isum  39144  pimdecfgtioo  39428  pimincfltioo  39429  iccpartipre  39784  bgoldbtbndlem2  40047
  Copyright terms: Public domain W3C validator