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

Theorem syl5ss 3809
Description: Subclass transitivity deduction. (Contributed by NM, 6-Feb-2014.)
Hypotheses
Ref Expression
syl5ss.1 𝐴𝐵
syl5ss.2 (𝜑𝐵𝐶)
Assertion
Ref Expression
syl5ss (𝜑𝐴𝐶)

Proof of Theorem syl5ss
StepHypRef Expression
1 syl5ss.1 . . 3 𝐴𝐵
21a1i 11 . 2 (𝜑𝐴𝐵)
3 syl5ss.2 . 2 (𝜑𝐵𝐶)
42, 3sstrd 3808 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3769
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 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-ext 2784
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 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-in 3776  df-ss 3783
This theorem is referenced by:  difsymssdifssd  4054  wereu2  5308  sofld  5792  fvmptss  6513  fimacnv  6569  isofr2  6818  frxp  7521  fnse  7528  smores2  7687  f1imaen2g  8253  domunsncan  8299  dffi3  8576  marypha1lem  8578  ordtypelem7  8668  ordtypelem8  8669  oismo  8684  unxpwdom2  8732  cantnfres  8821  oemapvali  8828  tskwe  9059  acndom2  9160  dfac2a  9235  dfac12lem2  9251  cfle  9361  cofsmo  9376  coftr  9380  isf34lem5  9485  isf34lem7  9486  isf34lem6  9487  enfin1ai  9491  fin1a2lem12  9518  ttukeylem7  9622  alephexp1  9686  fpwwe2lem13  9749  fpwwe2  9750  canth4  9754  canthwelem  9757  pwfseqlem1  9765  pwfseqlem4  9769  fzossnn0  12723  fsuppmapnn0fiublem  13013  fsuppmapnn0fiub  13014  xptrrel  13944  limsupgle  14431  limsupgre  14435  rlimres  14512  lo1res  14513  lo1resb  14518  rlimresb  14519  o1resb  14520  o1of2  14566  o1rlimmul  14572  isercolllem2  14619  isercoll  14621  climsup  14623  fprodntriv  14893  bitsinvp1  15390  sadcaddlem  15398  sadadd2lem  15400  sadadd3  15402  sadasslem  15411  sadeq  15413  bitsres  15414  smuval2  15423  smupval  15429  smueqlem  15431  smumul  15434  1arith  15848  isstruct2  16078  setscom  16114  ressress  16150  imasvscafn  16402  imasless  16405  mrcssv  16479  isacs1i  16522  mreacs  16523  acsfn  16524  isacs4lem  17373  isacs5lem  17374  mhmima  17568  cntzmhm  17972  f1omvdconj  18067  f1omvdco2  18069  symgsssg  18088  symggen  18091  psgnunilem1  18114  efgval  18331  gsumzaddlem  18522  gsumconst  18535  dmdprdd  18600  dprdfeq0  18623  dprdres  18629  dprdss  18630  dprdz  18631  subgdmdprd  18635  dprddisj2  18640  dprd2dlem1  18642  dprd2da  18643  dprd2d2  18645  dmdprdsplit2lem  18646  lmhmlsp  19256  lsppratlem4  19359  islbs3  19364  lbsextlem3  19369  mplcoe5  19677  mplind  19710  znleval  20110  evpmss  20139  frlmsslsp  20345  lindff1  20369  lindfrn  20370  f1lindf  20371  lindfmm  20376  lsslindf  20379  basdif0  20971  tgcl  20987  ppttop  21025  epttop  21027  ntrin  21079  mretopd  21110  neiptoptop  21149  cnclsi  21290  cnconst2  21301  cnrest2  21304  cnpresti  21306  cnprest2  21308  fiuncmp  21421  connsub  21438  connima  21442  iunconnlem  21444  1stcfb  21462  2ndc1stc  21468  2ndcdisj  21473  kgentopon  21555  llycmpkgen2  21567  1stckgenlem  21570  kgencn3  21575  ptclsg  21632  ptcnplem  21638  txtube  21657  hausdiag  21662  txkgen  21669  xkoco1cn  21674  xkoco2cn  21675  xkococnlem  21676  qtoptop2  21716  basqtop  21728  imastopn  21737  hmeores  21788  hmphdis  21813  ptcmpfi  21830  fbssfi  21854  filin  21871  infil  21880  fbasrn  21901  fgtr  21907  elfm  21964  imaelfm  21968  hausflim  21998  flimclslem  22001  fclscmp  22047  cnextcn  22084  tmdgsum2  22113  tgpconncomp  22129  ustexsym  22232  ustund  22238  ustimasn  22245  utoptop  22251  utopbas  22252  restutopopn  22255  blin2  22447  metustexhalf  22574  icccmplem2  22839  icccmplem3  22840  reconnlem2  22843  tchcph  23248  fmcfil  23282  resscdrg  23366  ivthlem2  23433  ivthlem3  23434  ivth2  23436  ovolfiniun  23482  ovoliunlem1  23483  ismbl2  23508  nulmbl2  23517  unmbl  23518  shftmbl  23519  voliunlem1  23531  voliunlem2  23532  ioombl1lem4  23542  uniioombllem4  23567  dyadmbllem  23580  dyadmbl  23581  mbflimsup  23647  i1fima  23659  i1fima2  23660  i1fadd  23676  itg1addlem4  23680  itg2splitlem  23729  itg2split  23730  ellimc3  23857  limcflflem  23858  limcflf  23859  limcresi  23863  limciun  23872  dvreslem  23887  dvres2lem  23888  dvres  23889  dvaddbr  23915  dvmulbr  23916  dvlip  23970  dvlip2  23972  c1liplem1  23973  dvivthlem1  23985  dvne0  23988  lhop1lem  23990  lhop  23993  dvcnvrelem1  23994  dvcnvrelem2  23995  dvfsumle  23998  dvfsumabs  24000  dvfsumlem2  24004  itgsubstlem  24025  mdegleb  24038  mdeglt  24039  mdegldg  24040  mdegxrcl  24041  mdegcl  24043  ig1peu  24145  reeff1olem  24414  logccv  24623  rlimcnp2  24907  lgamgulmlem2  24970  ppisval  25044  prmdvdsfi  25047  mumul  25121  sqff1o  25122  chtlepsi  25145  chpub  25159  dchrisum0lem2a  25420  pntlem3  25512  ex-res  27629  htthlem  28102  chlejb1i  28663  ssmd2  29499  fimarab  29772  fz2ssnn0  29874  gsumle  30104  locfinreflem  30232  sibfof  30727  sitgclbn  30730  sitgaddlemb  30735  eulerpartlemgu  30764  ballotlemsima  30902  reprinrn  31021  bnj1311  31415  erdsze2lem2  31509  iccllysconn  31555  cvmopnlem  31583  msrf  31762  frpomin  32059  frrlem4  32104  nosupno  32170  neiin  32648  neibastop1  32675  neibastop2lem  32676  topmeet  32680  poimirlem1  33723  poimirlem2  33724  poimirlem3  33725  poimirlem11  33733  poimirlem12  33734  poimirlem16  33738  poimirlem19  33741  poimirlem30  33752  cnambfre  33770  itg2gt0cn  33777  sstotbnd2  33884  sstotbnd3  33886  ssbnd  33898  ismtyima  33913  heibor1lem  33919  idresssidinxp  34395  pmodlem2  35627  pmodN  35630  diaintclN  36839  djaclN  36917  dibintclN  36948  dicval  36957  dihoml4c  37157  djhcl  37181  isnacs2  37771  isnacs3  37775  diophrw  37824  pellfundre  37947  pellfundge  37948  pellfundlb  37950  pellfundglb  37951  fnwe2lem2  38122  lmhmfgima  38155  hbt  38201  cnvtrcl0  38433  trclrelexplem  38503  relexp0a  38508  rp-imass  38565  isotone2  38847  climinf  40318  islptre  40331  limccog  40332  limcleqr  40356  itgcoscmulx  40664  ismbl3  40682  ismbl4  40689  stoweidlem27  40723  dirkercncflem2  40800  fourierdlem38  40841  fourierdlem49  40851  fourierdlem51  40853  fourierdlem54  40856  fourierdlem63  40865  fourierdlem68  40870  fourierdlem69  40871  fourierdlem70  40872  fourierdlem74  40876  fourierdlem75  40877  fourierdlem76  40878  fourierdlem80  40882  fourierdlem84  40886  fourierdlem85  40887  fourierdlem88  40890  fourierdlem100  40902  fourierdlem101  40903  fourierdlem104  40906  fourierdlem107  40909  fourierdlem111  40913  fourierdlem112  40914  caragenel2d  41228  hoidmv1lelem3  41289  hspmbllem3  41324  sssmf  41429  smfrec  41478  smfsuplem1  41499  mgmhmima  42370
  Copyright terms: Public domain W3C validator