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

Theorem syl5ss 3599
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 3598 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3560
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-in 3567  df-ss 3574
This theorem is referenced by:  wereu2  5081  sofld  5550  fvmptss  6259  fimacnv  6313  isofr2  6559  frxp  7247  fnse  7254  smores2  7411  f1imaen2g  7977  domunsncan  8020  dffi3  8297  marypha1lem  8299  ordtypelem7  8389  ordtypelem8  8390  oismo  8405  unxpwdom2  8453  cantnfres  8534  oemapvali  8541  tskwe  8736  acndom2  8837  dfac2a  8912  dfac12lem2  8926  cfle  9036  cofsmo  9051  coftr  9055  isf34lem5  9160  isf34lem7  9161  isf34lem6  9162  enfin1ai  9166  fin1a2lem12  9193  ttukeylem7  9297  alephexp1  9361  fpwwe2lem13  9424  fpwwe2  9425  canth4  9429  canthwelem  9432  pwfseqlem1  9440  pwfseqlem4  9444  fzossnn0  12456  fsuppmapnn0fiublem  12745  fsuppmapnn0fiub  12746  fsuppmapnn0fiubOLD  12747  xptrrel  13669  limsupgle  14158  limsupgre  14162  rlimres  14239  lo1res  14240  lo1resb  14245  rlimresb  14246  o1resb  14247  o1of2  14293  o1rlimmul  14299  isercolllem2  14346  isercoll  14348  climsup  14350  fprodntriv  14616  bitsinvp1  15114  sadcaddlem  15122  sadadd2lem  15124  sadadd3  15126  sadasslem  15135  sadeq  15137  bitsres  15138  smuval2  15147  smupval  15153  smueqlem  15155  smumul  15158  1arith  15574  isstruct2  15809  setscom  15843  ressress  15878  imasvscafn  16137  imasless  16140  mrcssv  16214  isacs1i  16258  mreacs  16259  acsfn  16260  isacs4lem  17108  isacs5lem  17109  mhmima  17303  cntzmhm  17711  f1omvdconj  17806  f1omvdco2  17808  symgsssg  17827  symggen  17830  psgnunilem1  17853  efgval  18070  gsumzaddlem  18261  gsumconst  18274  dmdprdd  18338  dprdfeq0  18361  dprdres  18367  dprdss  18368  dprdz  18369  subgdmdprd  18373  dprddisj2  18378  dprd2dlem1  18380  dprd2da  18381  dprd2d2  18383  dmdprdsplit2lem  18384  lmhmlsp  18989  lsppratlem4  19090  islbs3  19095  lbsextlem3  19100  mplcoe5  19408  mplind  19442  znleval  19843  evpmss  19872  frlmsslsp  20075  lindff1  20099  lindfrn  20100  f1lindf  20101  lindfmm  20106  lsslindf  20109  basdif0  20697  tgcl  20713  ppttop  20751  epttop  20753  ntrin  20805  mretopd  20836  neiptoptop  20875  cnclsi  21016  cnconst2  21027  cnrest2  21030  cnpresti  21032  cnprest2  21034  fiuncmp  21147  connsub  21164  connima  21168  iunconnlem  21170  1stcfb  21188  2ndc1stc  21194  2ndcdisj  21199  kgentopon  21281  llycmpkgen2  21293  1stckgenlem  21296  kgencn3  21301  ptclsg  21358  ptcnplem  21364  txtube  21383  hausdiag  21388  txkgen  21395  xkoco1cn  21400  xkoco2cn  21401  xkococnlem  21402  qtoptop2  21442  basqtop  21454  imastopn  21463  hmeores  21514  hmphdis  21539  ptcmpfi  21556  fbssfi  21581  filin  21598  infil  21607  fbasrn  21628  fgtr  21634  elfm  21691  imaelfm  21695  hausflim  21725  flimclslem  21728  fclscmp  21774  cnextcn  21811  tmdgsum2  21840  tgpconncomp  21856  ustexsym  21959  ustund  21965  ustimasn  21972  utoptop  21978  utopbas  21979  restutopopn  21982  blin2  22174  metustexhalf  22301  icccmplem2  22566  icccmplem3  22567  reconnlem2  22570  tchcph  22976  fmcfil  23010  resscdrg  23094  ivthlem2  23161  ivthlem3  23162  ivth2  23164  ovolfiniun  23209  ovoliunlem1  23210  ismbl2  23235  nulmbl2  23244  unmbl  23245  shftmbl  23246  voliunlem1  23258  voliunlem2  23259  ioombl1lem4  23269  uniioombllem4  23294  dyadmbllem  23307  dyadmbl  23308  mbflimsup  23373  i1fima  23385  i1fima2  23386  i1fadd  23402  itg1addlem4  23406  itg2splitlem  23455  itg2split  23456  ellimc3  23583  limcflflem  23584  limcflf  23585  limcresi  23589  limciun  23598  dvreslem  23613  dvres2lem  23614  dvres  23615  dvaddbr  23641  dvmulbr  23642  dvlip  23694  dvlip2  23696  c1liplem1  23697  dvivthlem1  23709  dvne0  23712  lhop1lem  23714  lhop  23717  dvcnvrelem1  23718  dvcnvrelem2  23719  dvfsumle  23722  dvfsumabs  23724  dvfsumlem2  23728  itgsubstlem  23749  mdegleb  23762  mdeglt  23763  mdegldg  23764  mdegxrcl  23765  mdegcl  23767  ig1peu  23869  reeff1olem  24138  logccv  24343  rlimcnp2  24627  lgamgulmlem2  24690  ppisval  24764  prmdvdsfi  24767  mumul  24841  sqff1o  24842  chtlepsi  24865  chpub  24879  dchrisum0lem2a  25140  pntlem3  25232  extwwlkfablem2  27102  ex-res  27186  htthlem  27662  chlejb1i  28223  ssmd2  29059  fimarab  29328  gsumle  29606  locfinreflem  29731  sibfof  30225  sitgclbn  30228  sitgaddlemb  30233  eulerpartlemgu  30262  ballotlemsima  30400  bnj1311  30853  erdsze2lem2  30947  iccllysconn  30993  cvmopnlem  31021  msrf  31200  nodenselem6  31602  nosino  31628  neiin  32022  neibastop1  32049  neibastop2lem  32050  topmeet  32054  poimirlem1  33081  poimirlem2  33082  poimirlem3  33083  poimirlem11  33091  poimirlem12  33092  poimirlem16  33096  poimirlem19  33099  poimirlem30  33110  cnambfre  33129  itg2gt0cn  33136  sstotbnd2  33244  sstotbnd3  33246  ssbnd  33258  ismtyima  33273  heibor1lem  33279  pmodlem2  34652  pmodN  34655  diaintclN  35866  djaclN  35944  dibintclN  35975  dicval  35984  dihoml4c  36184  djhcl  36208  isnacs2  36788  isnacs3  36792  diophrw  36841  pellfundre  36964  pellfundge  36965  pellfundlb  36967  pellfundglb  36968  fnwe2lem2  37140  lmhmfgima  37173  hbt  37220  cnvtrcl0  37453  trclrelexplem  37523  relexp0a  37528  rp-imass  37586  isotone2  37868  climinf  39274  islptre  39287  limccog  39288  limcleqr  39312  itgcoscmulx  39522  ismbl3  39540  ismbl4  39547  stoweidlem27  39581  dirkercncflem2  39658  fourierdlem38  39699  fourierdlem49  39709  fourierdlem51  39711  fourierdlem54  39714  fourierdlem63  39723  fourierdlem68  39728  fourierdlem69  39729  fourierdlem70  39730  fourierdlem74  39734  fourierdlem75  39735  fourierdlem76  39736  fourierdlem80  39740  fourierdlem84  39744  fourierdlem85  39745  fourierdlem88  39748  fourierdlem100  39760  fourierdlem101  39761  fourierdlem104  39764  fourierdlem107  39767  fourierdlem111  39771  fourierdlem112  39772  caragenel2d  40083  hoidmv1lelem3  40144  hspmbllem3  40179  sssmf  40284  smfrec  40333  smfsuplem1  40354  mgmhmima  41120
  Copyright terms: Public domain W3C validator