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

Theorem syl6ss 3821
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 3819 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3780
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-ext 2795
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-in 3787  df-ss 3794
This theorem is referenced by:  difss2  3949  rintn0  4822  eqbrrdva  5507  ssxpb  5793  relfld  5889  funssxp  6286  dff2  6603  dff3  6604  fliftf  6799  1stcof  7438  2ndcof  7439  nnunifi  8460  elfiun  8585  marypha1lem  8588  marypha1  8589  ordtypelem7  8678  tcmin  8874  unwf  8930  rankfu  8997  tcrank  9004  aceq3lem  9236  dfac12lem2  9261  ackbij1lem9  9345  ackbij1lem10  9346  ackbij1lem16  9352  fin23lem26  9442  fin23lem27  9445  fin1a2lem6  9522  itunitc  9538  axdc3lem2  9568  ttukeylem5  9630  fpwwe2lem13  9759  canthwelem  9767  pwfseqlem4  9779  wunex2  9855  wunex3  9858  inar1  9892  inatsk  9895  gruina  9935  suprfinzcl  11778  suprzub  12018  uzsupss  12019  uzwo3  12022  rpnnen1lem4  12056  rpnnen1lem5  12057  supxrre  12395  infxrre  12404  ioodisj  12545  supicclub2  12566  fzssnn  12628  fzossnn0  12743  elfzom1elp1fzo  12779  injresinjlem  12832  uzindi  13025  ssnn0fi  13028  seqcoll  13485  seqcoll2  13486  reltrclfv  14001  relexpdmg  14025  relexpdm  14026  relexprng  14029  relexprn  14030  relexpfld  14032  relexpaddg  14036  limsupval2  14454  limsupgre  14455  limsupbnd2  14457  rlimuni  14524  rlimcld2  14552  rlimno1  14627  isercolllem2  14639  isercoll  14641  summolem2a  14689  summolem2  14690  fsumsers  14702  fsumcvg3  14703  prodmolem2a  14905  prodmolem2  14906  zprod  14908  lcmfnnval  15576  lcmfnncl  15581  4sqlem11  15896  vdwlem8  15929  vdwlem11  15932  ramub2  15955  0ram  15961  0ram2  15962  0ramcl  15964  ramub1lem2  15968  prmgaplem3  15994  prmgaplem4  15995  isohom  16660  funcres2c  16785  resscntz  17985  cntzidss  17991  cntzmhm2  17993  pgpssslw  18250  cntzspan  18468  gsumval3  18529  gsum2d  18592  dprdspan  18648  dprdres  18649  lssintcl  19191  lbsextlem2  19388  lbsextlem3  19389  lbsextlem4  19390  islinds3  20404  fctop  21043  cctop  21045  neitr  21219  ordtbas2  21230  ordtopn1  21233  ordtopn2  21234  lmss  21337  clsconn  21468  2ndcdisj  21494  2ndcomap  21496  ptbasfi  21619  txcmplem2  21680  hausdiag  21683  txkgen  21690  basqtop  21749  alexsubb  22084  alexsubALTlem4  22088  tsmsres  22181  tsmsxplem1  22190  tsmsxp  22192  ustrel  22249  utop3cls  22289  prdsmet  22409  metustrel  22591  icccmplem2  22860  xrge0tsms  22871  cnmptre  22960  icchmeo  22974  bndth  22991  lebnumlem2  22995  cfilresi  23327  causs  23330  bcthlem5  23359  evthicc  23463  ovolficcss  23473  ovolmge0  23481  ovolgelb  23484  ovollb2lem  23492  ovollb2  23493  ovolunlem1a  23500  ovolunlem1  23501  ovoliunlem1  23506  ovoliunlem2  23507  ovoliun  23509  ovolscalem1  23517  ovolicc1  23520  ovolicc2lem4  23524  ovolicc2  23526  voliunlem2  23555  voliunlem3  23556  ioombl1lem2  23563  ioombl1lem4  23565  uniioovol  23583  uniiccvol  23584  uniioombllem1  23585  uniioombllem2  23587  uniioombllem3  23589  uniioombllem4  23590  uniioombllem6  23592  dyadmbllem  23603  dyadmbl  23604  volcn  23610  vitalilem4  23615  vitalilem5  23616  cnmbf  23663  i1fmul  23700  itg1addlem4  23703  itg2seq  23746  dvbssntr  23901  dvreslem  23910  dvcjbr  23949  dvferm1  23985  dvferm2  23987  cmvth  23991  dvlip  23993  lhop1lem  24013  lhop2  24015  lhop  24016  dvcnvrelem2  24018  dvcnvre  24019  dvfsumle  24021  dvfsumge  24022  dvfsumabs  24023  dvfsumlem2  24027  ftc1a  24037  ftc1lem3  24038  ftc1lem6  24041  itgsubstlem  24048  mdegleb  24061  mdeglt  24062  mdegldg  24063  mdegxrcl  24064  mdegcl  24066  deg1mul3le  24113  ig1pdvds  24173  plyeq0lem  24203  aannenlem2  24321  aalioulem3  24326  taylf  24352  taylthlem2  24365  pserulm  24413  psercn2  24414  psercn  24417  reeff1olem  24437  efcvx  24440  loglesqrt  24736  rlimcnp  24929  xrlimcnp  24932  jensen  24952  wilthlem2  25032  vmadivsumb  25409  pntrsumo1  25491  pntlem3  25535  perpln2  25843  axcontlem10  26090  usgrexmplef  26390  nmoxr  27972  nmooge0  27973  nmoolb  27977  nmoubi  27978  ubthlem1  28077  shmodi  28600  nmopxr  29076  nmfnxr  29089  nmoplb  29117  nmopub  29118  nmfnlb  29134  nmfnleub  29135  nmopun  29224  branmfn  29315  mdslj1i  29529  hatomistici  29572  xppreima2  29800  fpwrelmap  29858  infxrge0gelb  29881  xrge0tsmsd  30133  metideq  30284  metider  30285  pstmfval  30287  esumgect  30500  esum2d  30503  sigaclci  30543  insiga  30548  omssubadd  30710  eulerpartlemgs2  30790  ballotlemsima  30925  signsply0  30976  iblidicc  31018  fsum2dsub  31033  reprsuc  31041  reprgt  31047  bnj1145  31406  bnj1137  31408  bnj1136  31410  resconn  31573  cvmliftlem8  31619  cvmlift3lem6  31651  mclsssvlem  31804  mclsind  31812  mclsppslem  31825  nosupbday  32194  ivthALT  32673  neibastop1  32697  topjoin  32703  ptrecube  33741  poimirlem6  33747  poimirlem15  33756  heicant  33776  mblfinlem2  33779  mblfinlem3  33780  mblfinlem4  33781  ismblfin  33782  itg2gt0cn  33796  ftc1cnnc  33815  ftc1anclem3  33818  ftc1anclem7  33822  ftc1anclem8  33823  ftc1anc  33824  areacirclem2  33832  areacirclem3  33833  areacirclem4  33834  totbndbnd  33918  prdsbnd  33922  heiborlem1  33940  rrnequiv  33964  reheibor  33968  iccbnd  33969  pmapssbaN  35559  2polssN  35714  paddunN  35726  poldmj1N  35727  ispsubcl2N  35746  psubclinN  35747  paddatclN  35748  poml4N  35752  diaglbN  36854  diaintclN  36857  dibglbN  36965  dibintclN  36966  dicssdvh  36985  dihvalrel  37078  dochexmidlem4  37262  rmxyelqirr  37994  ttac  38122  hbtlem6  38218  hbt  38219  itgpowd  38318  cnvssb  38410  cnvrcl0  38450  cnvtrrel  38480  relexpaddss  38528  cotrcltrcl  38535  cotrclrcl  38552  frege96d  38559  frege97d  38562  frege109d  38567  frege131d  38574  rp-imass  38583  rfovcnvf1od  38816  isotone2  38865  gneispace  38950  k0004ss1  38967  uzfissfz  40040  suplesup  40053  limciccioolb  40351  limcicciooub  40367  limcleqr  40374  cnrefiisplem  40553  cncfiooicclem1  40604  ibliccsinexp  40664  iblioosinexp  40666  itgcoscmulx  40682  itgsincmulx  40687  itgsubsticclem  40688  itgiccshift  40693  itgperiod  40694  itgsbtaddcnst  40695  stoweidlem34  40748  stoweidlem59  40773  dirkeritg  40816  dirkercncflem2  40818  fourierdlem20  40841  fourierdlem31  40852  fourierdlem39  40860  fourierdlem42  40863  fourierdlem46  40866  fourierdlem52  40872  fourierdlem53  40873  fourierdlem60  40880  fourierdlem61  40881  fourierdlem62  40882  fourierdlem68  40888  fourierdlem76  40896  fourierdlem85  40905  fourierdlem88  40908  fourierdlem89  40909  fourierdlem90  40910  fourierdlem91  40911  fourierdlem93  40913  fourierdlem94  40914  fourierdlem103  40923  fourierdlem104  40924  fourierdlem111  40931  fouriersw  40945  etransclem46  40994  etransclem48  40996  sge0less  41106  sge0resplit  41120  sge0isum  41141  pimdecfgtioo  41427  pimincfltioo  41428  iccpartipre  41950  bgoldbtbndlem2  42287  setrec1lem4  43023  setrec2fun  43025
  Copyright terms: Public domain W3C validator