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

Theorem syl6ss 3648
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 3646 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3607
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-in 3614  df-ss 3621
This theorem is referenced by:  difss2  3772  rintn0  4651  eqbrrdva  5324  ssxpb  5603  relfld  5699  funssxp  6099  dff2  6411  dff3  6412  fliftf  6605  1stcof  7240  2ndcof  7241  nnunifi  8252  elfiun  8377  marypha1lem  8380  marypha1  8381  ordtypelem7  8470  tcmin  8655  unwf  8711  rankfu  8778  tcrank  8785  aceq3lem  8981  dfac12lem2  9004  ackbij1lem9  9088  ackbij1lem10  9089  ackbij1lem16  9095  fin23lem26  9185  fin23lem27  9188  fin1a2lem6  9265  itunitc  9281  axdc3lem2  9311  ttukeylem5  9373  fpwwe2lem13  9502  canthwelem  9510  pwfseqlem4  9522  wunex2  9598  wunex3  9601  inar1  9635  inatsk  9638  gruina  9678  suprfinzcl  11530  suprzub  11817  uzsupss  11818  uzwo3  11821  rpnnen1lem4  11855  rpnnen1lem5  11856  rpnnen1lem4OLD  11861  rpnnen1lem5OLD  11862  supxrre  12195  infxrre  12204  ioodisj  12340  supicclub2  12361  fzssnn  12423  fzossnn0  12538  elfzom1elp1fzo  12574  injresinjlem  12628  uzindi  12821  ssnn0fi  12824  seqcoll  13286  seqcoll2  13287  reltrclfv  13802  relexpdmg  13826  relexpdm  13827  relexprng  13830  relexprn  13831  relexpfld  13833  relexpaddg  13837  limsupval2  14255  limsupgre  14256  limsupbnd2  14258  rlimuni  14325  rlimcld2  14353  rlimno1  14428  isercolllem2  14440  isercoll  14442  summolem2a  14490  summolem2  14491  fsumsers  14503  fsumcvg3  14504  prodmolem2a  14708  prodmolem2  14709  zprod  14711  lcmfnnval  15384  lcmfnncl  15389  4sqlem11  15706  vdwlem8  15739  vdwlem11  15742  ramub2  15765  0ram  15771  0ram2  15772  0ramcl  15774  ramub1lem2  15778  prmgaplem3  15804  prmgaplem4  15805  isohom  16483  funcres2c  16608  resscntz  17810  cntzidss  17816  cntzmhm2  17818  pgpssslw  18075  cntzspan  18293  gsumval3  18354  gsum2d  18417  dprdspan  18472  dprdres  18473  lssintcl  19012  lbsextlem2  19207  lbsextlem3  19208  lbsextlem4  19209  mplbas2  19518  islinds3  20221  fctop  20856  cctop  20858  neitr  21032  ordtbas2  21043  ordtopn1  21046  ordtopn2  21047  lmss  21150  clsconn  21281  2ndcdisj  21307  2ndcomap  21309  ptbasfi  21432  txcmplem2  21493  hausdiag  21496  txkgen  21503  basqtop  21562  alexsubb  21897  alexsubALTlem4  21901  tsmsres  21994  tsmsxplem1  22003  tsmsxp  22005  ustrel  22062  utop3cls  22102  prdsmet  22222  metustrel  22404  icccmplem2  22673  xrge0tsms  22684  cnmptre  22773  icchmeo  22787  bndth  22804  lebnumlem2  22808  cfilresi  23139  causs  23142  bcthlem5  23171  evthicc  23274  ovolficcss  23284  ovolmge0  23291  ovolgelb  23294  ovollb2lem  23302  ovollb2  23303  ovolunlem1a  23310  ovolunlem1  23311  ovoliunlem1  23316  ovoliunlem2  23317  ovoliun  23319  ovolscalem1  23327  ovolicc1  23330  ovolicc2lem4  23334  ovolicc2  23336  voliunlem2  23365  voliunlem3  23366  ioombl1lem2  23373  ioombl1lem4  23375  uniioovol  23393  uniiccvol  23394  uniioombllem1  23395  uniioombllem2  23397  uniioombllem3  23399  uniioombllem4  23400  uniioombllem6  23402  dyadmbllem  23413  dyadmbl  23414  volcn  23420  vitalilem4  23425  vitalilem5  23426  cnmbf  23471  i1fmul  23508  itg1addlem4  23511  itg2seq  23554  dvbssntr  23709  dvreslem  23718  dvcjbr  23757  dvferm1  23793  dvferm2  23795  cmvth  23799  dvlip  23801  lhop1lem  23821  lhop2  23823  lhop  23824  dvcnvrelem2  23826  dvcnvre  23827  dvfsumle  23829  dvfsumge  23830  dvfsumabs  23831  dvfsumlem2  23835  ftc1a  23845  ftc1lem3  23846  ftc1lem6  23849  itgsubstlem  23856  mdegleb  23869  mdeglt  23870  mdegldg  23871  mdegxrcl  23872  mdegcl  23874  deg1mul3le  23921  ig1pdvds  23981  plyeq0lem  24011  aannenlem2  24129  aalioulem3  24134  taylf  24160  taylthlem2  24173  pserulm  24221  psercn2  24222  psercn  24225  reeff1olem  24245  efcvx  24248  loglesqrt  24544  rlimcnp  24737  xrlimcnp  24740  jensen  24760  wilthlem2  24840  vmadivsumb  25217  pntrsumo1  25299  pntlem3  25343  perpln2  25651  axcontlem10  25898  usgrexmplef  26196  nmoxr  27749  nmooge0  27750  nmoolb  27754  nmoubi  27755  ubthlem1  27854  shmodi  28377  nmopxr  28853  nmfnxr  28866  nmoplb  28894  nmopub  28895  nmfnlb  28911  nmfnleub  28912  nmopun  29001  branmfn  29092  mdslj1i  29306  hatomistici  29349  xppreima2  29578  fpwrelmap  29636  infxrge0gelb  29659  xrge0tsmsd  29913  metideq  30064  metider  30065  pstmfval  30067  esumgect  30280  esum2d  30283  sigaclci  30323  insiga  30328  omssubadd  30490  eulerpartlemgs2  30570  ballotlemsima  30705  signsply0  30756  iblidicc  30798  fsum2dsub  30813  reprsuc  30821  reprgt  30827  bnj1145  31187  bnj1137  31189  bnj1136  31191  resconn  31354  cvmliftlem8  31400  cvmlift3lem6  31432  mclsssvlem  31585  mclsind  31593  mclsppslem  31606  nosupbday  31976  ivthALT  32455  neibastop1  32479  topjoin  32485  ptrecube  33539  poimirlem6  33545  poimirlem15  33554  heicant  33574  mblfinlem2  33577  mblfinlem3  33578  mblfinlem4  33579  ismblfin  33580  itg2gt0cn  33595  ftc1cnnc  33614  ftc1anclem3  33617  ftc1anclem7  33621  ftc1anclem8  33622  ftc1anc  33623  areacirclem2  33631  areacirclem3  33632  areacirclem4  33633  totbndbnd  33718  prdsbnd  33722  heiborlem1  33740  rrnequiv  33764  reheibor  33768  iccbnd  33769  pmapssbaN  35364  2polssN  35519  paddunN  35531  poldmj1N  35532  ispsubcl2N  35551  psubclinN  35552  paddatclN  35553  poml4N  35557  diaglbN  36661  diaintclN  36664  dibglbN  36772  dibintclN  36773  dicssdvh  36792  dihvalrel  36885  dochexmidlem4  37069  rmxyelqirr  37792  ttac  37920  hbtlem6  38016  hbt  38017  itgpowd  38117  cnvssb  38209  cnvrcl0  38249  cnvtrrel  38279  relexpaddss  38327  cotrcltrcl  38334  cotrclrcl  38351  frege96d  38358  frege97d  38361  frege109d  38366  frege131d  38373  rp-imass  38382  rfovcnvf1od  38615  isotone2  38664  gneispace  38749  k0004ss1  38766  uzfissfz  39855  suplesup  39868  limciccioolb  40171  limcicciooub  40187  limcleqr  40194  cnrefiisplem  40373  cncfiooicclem1  40424  ibliccsinexp  40484  iblioosinexp  40486  itgcoscmulx  40503  itgsincmulx  40508  itgsubsticclem  40509  itgiccshift  40514  itgperiod  40515  itgsbtaddcnst  40516  stoweidlem34  40569  stoweidlem59  40594  dirkeritg  40637  dirkercncflem2  40639  fourierdlem20  40662  fourierdlem31  40673  fourierdlem39  40681  fourierdlem42  40684  fourierdlem46  40687  fourierdlem52  40693  fourierdlem53  40694  fourierdlem60  40701  fourierdlem61  40702  fourierdlem62  40703  fourierdlem68  40709  fourierdlem76  40717  fourierdlem85  40726  fourierdlem88  40729  fourierdlem89  40730  fourierdlem90  40731  fourierdlem91  40732  fourierdlem93  40734  fourierdlem94  40735  fourierdlem103  40744  fourierdlem104  40745  fourierdlem111  40752  fouriersw  40766  etransclem46  40815  etransclem48  40817  sge0less  40927  sge0resplit  40941  sge0isum  40962  pimdecfgtioo  41248  pimincfltioo  41249  iccpartipre  41682  bgoldbtbndlem2  42019  setrec1lem4  42762  setrec2fun  42764
  Copyright terms: Public domain W3C validator