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

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

Proof of Theorem sstrid
StepHypRef Expression
1 sstrid.1 . . 3 𝐴𝐵
21a1i 11 . 2 (𝜑𝐴𝐵)
3 sstrid.2 . 2 (𝜑𝐵𝐶)
42, 3sstrd 3933 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3890
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811
This theorem depends on definitions:  df-bi 207  df-an 396  df-ss 3907
This theorem is referenced by:  difsymssdifssd  4205  wereu2  5621  sofld  6145  resssxp  6228  frpomin  6298  fimass  6682  fvmptss  6954  isofr2  7292  frxp  8069  fnse  8076  frxp2  8087  frxp3  8094  frrlem4  8232  frrlem13  8241  fprlem1  8243  smores2  8287  naddunif  8622  dffi3  9337  marypha1lem  9339  ordtypelem7  9432  ordtypelem8  9433  oismo  9448  unxpwdom2  9496  cantnfres  9589  oemapvali  9596  frmin  9664  frrlem15  9672  frrlem16  9673  tskwe  9865  acndom2  9967  dfac2a  10043  dfac12lem2  10058  cfle  10167  cofsmo  10182  coftr  10186  isf34lem5  10291  isf34lem7  10292  isf34lem6  10293  enfin1ai  10297  fin1a2lem12  10324  ttukeylem7  10428  alephexp1  10493  fpwwe2lem12  10556  fpwwe2  10557  canth4  10561  canthwelem  10564  pwfseqlem1  10572  pwfseqlem4  10576  fzossnn0  13636  fsuppmapnn0fiublem  13943  fsuppmapnn0fiub  13944  xptrrel  14933  limsupgle  15430  limsupgre  15434  rlimres  15511  lo1res  15512  lo1resb  15517  rlimresb  15518  o1resb  15519  o1of2  15566  o1rlimmul  15572  isercolllem2  15619  isercoll  15621  climsup  15623  fprodntriv  15898  bitsinvp1  16409  sadcaddlem  16417  sadadd2lem  16419  sadadd3  16421  sadasslem  16430  sadeq  16432  bitsres  16433  smuval2  16442  smupval  16448  smueqlem  16450  smumul  16453  1arith  16889  isstruct2  17110  setscom  17141  ressress  17208  imasvscafn  17492  imasless  17495  mrcssv  17571  isacs1i  17614  mreacs  17615  acsfn  17616  isacs4lem  18501  isacs5lem  18502  mgmhmima  18674  mhmima  18784  cntzmhm  19307  f1omvdconj  19412  f1omvdco2  19414  symgsssg  19433  symggen  19436  efgval  19683  gsumzaddlem  19887  gsumconst  19900  dmdprdd  19967  dprdfeq0  19990  dprdres  19996  dprdss  19997  dprdz  19998  subgdmdprd  20002  dprddisj2  20007  dprd2dlem1  20009  dprd2da  20010  dprd2d2  20012  dmdprdsplit2lem  20013  gsumle  20111  lmhmlsp  21036  lsppratlem4  21140  islbs3  21145  lbsextlem3  21150  znleval  21544  evpmss  21576  frlmsslsp  21786  lindff1  21810  lindfrn  21811  f1lindf  21812  lindfmm  21817  lsslindf  21820  mplcoe5  22028  mplind  22058  basdif0  22928  tgcl  22944  ppttop  22982  epttop  22984  ntrin  23036  mretopd  23067  neiptoptop  23106  cnclsi  23247  cnconst2  23258  cnrest2  23261  cnpresti  23263  cnprest2  23265  fiuncmp  23379  connsub  23396  connima  23400  iunconnlem  23402  1stcfb  23420  2ndc1stc  23426  2ndcdisj  23431  kgentopon  23513  llycmpkgen2  23525  1stckgenlem  23528  kgencn3  23533  ptclsg  23590  ptcnplem  23596  txtube  23615  hausdiag  23620  txkgen  23627  xkoco1cn  23632  xkoco2cn  23633  xkococnlem  23634  qtoptop2  23674  basqtop  23686  imastopn  23695  hmeores  23746  hmphdis  23771  ptcmpfi  23788  fbssfi  23812  filin  23829  infil  23838  fgtr  23865  elfm  23922  hausflim  23956  flimclslem  23959  fclscmp  24005  cnextcn  24042  tmdgsum2  24071  tgpconncomp  24088  ustexsym  24191  ustund  24197  ustimasn  24203  utoptop  24209  utopbas  24210  restutopopn  24213  blin2  24404  metustexhalf  24531  icccmplem2  24799  icccmplem3  24800  reconnlem2  24803  tcphcph  25214  fmcfil  25249  resscdrg  25335  ivthlem2  25429  ivthlem3  25430  ivth2  25432  ovolfiniun  25478  ovoliunlem1  25479  ismbl2  25504  nulmbl2  25513  unmbl  25514  shftmbl  25515  voliunlem1  25527  voliunlem2  25528  ioombl1lem4  25538  uniioombllem4  25563  uniioombllem5  25564  dyadmbllem  25576  dyadmbl  25577  mbflimsup  25643  i1fima  25655  i1fima2  25656  i1fadd  25672  itg1addlem4  25676  itg2splitlem  25725  itg2split  25726  ellimc3  25856  limcflflem  25857  limcflf  25858  limcresi  25862  limciun  25871  dvreslem  25886  dvres2lem  25887  dvres  25888  dvaddbr  25915  dvmulbr  25916  dvlip  25970  dvlip2  25972  c1liplem1  25973  dvivthlem1  25985  dvne0  25988  lhop1lem  25990  lhop  25993  dvcnvrelem1  25994  dvcnvrelem2  25995  dvfsumle  25998  dvfsumabs  26000  dvfsumlem2  26004  itgsubstlem  26025  mdegleb  26039  mdeglt  26040  mdegldg  26041  mdegxrcl  26042  mdegcl  26044  ig1peu  26150  reeff1olem  26424  logccv  26640  rlimcnp2  26943  lgamgulmlem2  27007  ppisval  27081  prmdvdsfi  27084  mumul  27158  sqff1o  27159  chtlepsi  27183  chpub  27197  dchrisum0lem2a  27494  pntlem3  27586  nosupno  27681  noetalem1  27719  cutlt  27938  negsproplem2  28035  onsbnd  28287  ex-res  30526  htthlem  31003  chlejb1i  31562  ssmd2  32398  fz2ssnn0  32873  gsumpart  33139  gsumhashmul  33143  elrgspnsubrunlem2  33324  extvfvcl  33695  mplvrpmrhm  33706  esplyind  33734  vietalem  33738  locfinreflem  34000  sibfof  34500  sitgclbn  34503  sitgaddlemb  34508  eulerpartlemgu  34537  ballotlemsima  34676  reprinrn  34778  bnj1311  35182  fnrelpredd  35250  erdsze2lem2  35402  iccllysconn  35448  cvmopnlem  35476  msrf  35740  neiin  36530  neibastop1  36557  neibastop2lem  36558  topmeet  36562  ttciunun  36709  poimirlem1  37956  poimirlem2  37957  poimirlem3  37958  poimirlem11  37966  poimirlem12  37967  poimirlem16  37971  poimirlem19  37974  poimirlem30  37985  cnambfre  38003  itg2gt0cn  38010  sstotbnd2  38109  sstotbnd3  38111  ssbnd  38123  ismtyima  38138  heibor1lem  38144  idresssidinxp  38649  pmodlem2  40307  pmodN  40310  diaintclN  41518  djaclN  41596  dibintclN  41627  dicval  41636  dihoml4c  41836  djhcl  41860  infdesc  43090  isnacs2  43152  isnacs3  43156  diophrw  43205  pellfundre  43327  pellfundge  43328  pellfundlb  43330  pellfundglb  43331  fnwe2lem2  43497  lmhmfgima  43530  hbt  43576  omabs2  43778  nadd2rabord  43831  nadd1rabord  43835  cnvtrcl0  44071  trclrelexplem  44156  relexp0a  44161  isotone2  44494  imo72b2lem1  44614  tcfr  45408  modelaxreplem1  45423  wfac8prim  45447  climinf  46054  islptre  46067  limccog  46068  limcleqr  46090  limsupvaluz2  46184  itgcoscmulx  46415  ismbl3  46432  ismbl4  46439  stoweidlem27  46473  dirkercncflem2  46550  fourierdlem38  46591  fourierdlem49  46601  fourierdlem51  46603  fourierdlem54  46606  fourierdlem63  46615  fourierdlem68  46620  fourierdlem69  46621  fourierdlem70  46622  fourierdlem74  46626  fourierdlem75  46627  fourierdlem76  46628  fourierdlem80  46632  fourierdlem84  46636  fourierdlem85  46637  fourierdlem88  46640  fourierdlem100  46652  fourierdlem101  46653  fourierdlem104  46656  fourierdlem107  46659  fourierdlem111  46663  fourierdlem112  46664  caragenel2d  46978  hoidmv1lelem3  47039  hspmbllem3  47074  sssmf  47184  smfrec  47235  smfsuplem1  47257
  Copyright terms: Public domain W3C validator