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

Theorem syl6ss 3866
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 3864 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3825
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-ext 2745
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-clab 2754  df-cleq 2765  df-clel 2840  df-in 3832  df-ss 3839
This theorem is referenced by:  difss2  3996  rintn0  4890  eqbrrdva  5583  ssxpb  5865  relfld  5958  funssxp  6358  dff2  6682  dff3  6683  fliftf  6885  1stcof  7524  2ndcof  7525  nnunifi  8556  elfiun  8681  marypha1lem  8684  marypha1  8685  ordtypelem7  8775  tcmin  8969  unwf  9025  rankfu  9092  tcrank  9099  aceq3lem  9332  dfac12lem2  9356  ackbij1lem9  9440  ackbij1lem10  9441  ackbij1lem16  9447  fin23lem26  9537  fin23lem27  9540  fin1a2lem6  9617  itunitc  9633  axdc3lem2  9663  ttukeylem5  9725  fpwwe2lem13  9854  canthwelem  9862  pwfseqlem4  9874  wunex2  9950  wunex3  9953  inar1  9987  inatsk  9990  gruina  10030  suprfinzcl  11903  suprzub  12146  uzsupss  12147  uzwo3  12150  rpnnen1lem4  12187  rpnnen1lem5  12188  supxrre  12529  infxrre  12538  ioodisj  12677  supicclub2  12698  fzssnn  12760  fzossnn0  12876  elfzom1elp1fzo  12912  injresinjlem  12965  uzindi  13158  ssnn0fi  13161  seqcoll  13625  seqcoll2  13626  reltrclfv  14228  relexpdmg  14252  relexpdm  14253  relexprng  14256  relexprn  14257  relexpfld  14259  relexpaddg  14263  limsupval2  14688  limsupgre  14689  limsupbnd2  14691  rlimuni  14758  rlimcld2  14786  rlimno1  14861  isercolllem2  14873  isercoll  14875  summolem2a  14922  summolem2  14923  fsumsers  14935  fsumcvg3  14936  prodmolem2a  15138  prodmolem2  15139  zprod  15141  lcmfnnval  15814  lcmfnncl  15819  4sqlem11  16137  vdwlem8  16170  vdwlem11  16173  ramub2  16196  0ram  16202  0ram2  16203  0ramcl  16205  ramub1lem2  16209  prmgaplem3  16235  prmgaplem4  16236  isohom  16894  funcres2c  17019  resscntz  18223  cntzidss  18229  cntzmhm2  18231  pgpssslw  18490  cntzspan  18710  gsumval3  18771  gsum2d  18835  dprdspan  18889  dprdres  18890  subdrgint  19294  sdrgint  19295  primefld  19296  lssintcl  19448  lbsextlem2  19643  lbsextlem3  19644  lbsextlem4  19645  islinds3  20670  fctop  21306  cctop  21308  neitr  21482  ordtbas2  21493  ordtopn1  21496  ordtopn2  21497  lmss  21600  clsconn  21732  2ndcdisj  21758  2ndcomap  21760  ptbasfi  21883  txcmplem2  21944  hausdiag  21947  txkgen  21954  basqtop  22013  alexsubb  22348  alexsubALTlem4  22352  tsmsres  22445  tsmsxplem1  22454  tsmsxp  22456  ustrel  22513  utop3cls  22553  prdsmet  22673  metustrel  22855  icccmplem2  23124  xrge0tsms  23135  cnmptre  23224  icchmeo  23238  bndth  23255  lebnumlem2  23259  cfilresi  23591  causs  23594  bcthlem5  23624  evthicc  23753  ovolficcss  23763  ovolmge0  23771  ovolgelb  23774  ovollb2lem  23782  ovollb2  23783  ovolunlem1a  23790  ovolunlem1  23791  ovoliunlem1  23796  ovoliunlem2  23797  ovoliun  23799  ovolscalem1  23807  ovolicc1  23810  ovolicc2lem4  23814  ovolicc2  23816  voliunlem2  23845  voliunlem3  23846  ioombl1lem2  23853  ioombl1lem4  23855  uniioovol  23873  uniiccvol  23874  uniioombllem1  23875  uniioombllem2  23877  uniioombllem3  23879  uniioombllem4  23880  uniioombllem6  23882  dyadmbllem  23893  dyadmbl  23894  volcn  23900  vitalilem4  23905  vitalilem5  23906  cnmbf  23953  i1fmul  23990  itg1addlem4  23993  itg2seq  24036  dvbssntr  24191  dvreslem  24200  dvcjbr  24239  dvferm1  24275  dvferm2  24277  cmvth  24281  dvlip  24283  lhop1lem  24303  lhop2  24305  lhop  24306  dvcnvrelem2  24308  dvcnvre  24309  dvfsumle  24311  dvfsumge  24312  dvfsumabs  24313  dvfsumlem2  24317  ftc1a  24327  ftc1lem3  24328  ftc1lem6  24331  itgsubstlem  24338  mdegleb  24351  mdeglt  24352  mdegldg  24353  mdegxrcl  24354  mdegcl  24356  deg1mul3le  24403  ig1pdvds  24463  plyeq0lem  24493  aannenlem2  24611  aalioulem3  24616  taylf  24642  taylthlem2  24655  pserulm  24703  psercn2  24704  psercn  24707  reeff1olem  24727  efcvx  24730  loglesqrt  25030  rlimcnp  25235  xrlimcnp  25238  jensen  25258  wilthlem2  25338  vmadivsumb  25751  pntrsumo1  25833  pntlem3  25877  perpln2  26189  axcontlem10  26452  usgrexmplef  26734  nmoxr  28310  nmooge0  28311  nmoolb  28315  nmoubi  28316  ubthlem1  28415  shmodi  28938  nmopxr  29414  nmfnxr  29427  nmoplb  29455  nmopub  29456  nmfnlb  29472  nmfnleub  29473  nmopun  29562  branmfn  29653  mdslj1i  29867  hatomistici  29910  xppreima2  30147  fsuppcurry1  30202  fsuppcurry2  30203  fpwrelmap  30210  infxrge0gelb  30231  prmdvdsbc  30267  xrge0tsmsd  30486  metideq  30734  metider  30735  pstmfval  30737  esumgect  30950  esum2d  30953  sigaclci  30993  insiga  30998  omssubadd  31160  eulerpartlemgs2  31240  ballotlemsima  31376  signsply0  31428  iblidicc  31472  fsum2dsub  31487  reprsuc  31495  reprgt  31501  bnj1145  31871  bnj1137  31873  bnj1136  31875  resconn  32038  cvmliftlem8  32084  cvmlift3lem6  32116  mclsssvlem  32269  mclsind  32277  mclsppslem  32290  frrlem13  32596  nosupbday  32666  ivthALT  33144  neibastop1  33168  topjoin  33174  ptrecube  34281  poimirlem6  34287  poimirlem15  34296  heicant  34316  mblfinlem2  34319  mblfinlem3  34320  mblfinlem4  34321  ismblfin  34322  itg2gt0cn  34336  ftc1cnnc  34355  ftc1anclem3  34358  ftc1anclem7  34362  ftc1anclem8  34363  ftc1anc  34364  areacirclem2  34372  areacirclem3  34373  areacirclem4  34374  totbndbnd  34457  prdsbnd  34461  heiborlem1  34479  rrnequiv  34503  reheibor  34507  iccbnd  34508  pmapssbaN  36289  2polssN  36444  paddunN  36456  poldmj1N  36457  ispsubcl2N  36476  psubclinN  36477  paddatclN  36478  poml4N  36482  diaglbN  37584  diaintclN  37587  dibglbN  37695  dibintclN  37696  dicssdvh  37715  dihvalrel  37808  dochexmidlem4  37992  rmxyelqirr  38848  ttac  38974  hbtlem6  39070  hbt  39071  itgpowd  39162  cnvssb  39253  cnvrcl0  39293  cnvtrrel  39323  relexpaddss  39371  cotrcltrcl  39378  cotrclrcl  39395  frege96d  39402  frege97d  39405  frege109d  39410  frege131d  39417  rp-imass  39425  rfovcnvf1od  39658  isotone2  39707  gneispace  39792  k0004ss1  39809  grumnudlem  39941  uzfissfz  40969  suplesup  40982  ssrexr  41083  limciccioolb  41279  limcicciooub  41295  limcleqr  41302  cnrefiisplem  41487  cncfiooicclem1  41552  ibliccsinexp  41612  iblioosinexp  41614  itgcoscmulx  41630  itgsincmulx  41635  itgsubsticclem  41636  itgiccshift  41641  itgperiod  41642  itgsbtaddcnst  41643  stoweidlem34  41696  stoweidlem59  41721  dirkeritg  41764  dirkercncflem2  41766  fourierdlem20  41789  fourierdlem31  41800  fourierdlem39  41808  fourierdlem42  41811  fourierdlem46  41814  fourierdlem52  41820  fourierdlem53  41821  fourierdlem60  41828  fourierdlem61  41829  fourierdlem62  41830  fourierdlem68  41836  fourierdlem76  41844  fourierdlem85  41853  fourierdlem88  41856  fourierdlem89  41857  fourierdlem90  41858  fourierdlem91  41859  fourierdlem93  41861  fourierdlem94  41862  fourierdlem103  41871  fourierdlem104  41872  fourierdlem111  41879  fouriersw  41893  etransclem46  41942  etransclem48  41944  sge0less  42051  sge0resplit  42065  sge0isum  42086  pimdecfgtioo  42372  pimincfltioo  42373  iccpartipre  42899  bgoldbtbndlem2  43279  setrec1lem4  44100  setrec2fun  44102
  Copyright terms: Public domain W3C validator