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

Theorem sstrid 3981
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 3980 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3939
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2152  ax-12 2167  ax-ext 2796
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2803  df-cleq 2817  df-clel 2897  df-in 3946  df-ss 3955
This theorem is referenced by:  difsymssdifssd  4233  wereu2  5550  sofld  6041  fimass  6551  fvmptss  6775  fimacnv  6834  isofr2  7092  frxp  7814  fnse  7821  smores2  7985  dffi3  8887  marypha1lem  8889  ordtypelem7  8980  ordtypelem8  8981  oismo  8996  unxpwdom2  9044  cantnfres  9132  oemapvali  9139  tskwe  9371  acndom2  9472  dfac2a  9547  dfac12lem2  9562  cfle  9668  cofsmo  9683  coftr  9687  isf34lem5  9792  isf34lem7  9793  isf34lem6  9794  enfin1ai  9798  fin1a2lem12  9825  ttukeylem7  9929  alephexp1  9993  fpwwe2lem13  10056  fpwwe2  10057  canth4  10061  canthwelem  10064  pwfseqlem1  10072  pwfseqlem4  10076  fzossnn0  13061  fsuppmapnn0fiublem  13351  fsuppmapnn0fiub  13352  xptrrel  14333  limsupgle  14827  limsupgre  14831  rlimres  14908  lo1res  14909  lo1resb  14914  rlimresb  14915  o1resb  14916  o1of2  14962  o1rlimmul  14968  isercolllem2  15015  isercoll  15017  climsup  15019  fprodntriv  15288  bitsinvp1  15790  sadcaddlem  15798  sadadd2lem  15800  sadadd3  15802  sadasslem  15811  sadeq  15813  bitsres  15814  smuval2  15823  smupval  15829  smueqlem  15831  smumul  15834  1arith  16255  isstruct2  16485  setscom  16519  ressress  16554  imasvscafn  16802  imasless  16805  mrcssv  16877  isacs1i  16920  mreacs  16921  acsfn  16922  isacs4lem  17770  isacs5lem  17771  mhmima  17974  cntzmhm  18401  f1omvdconj  18496  f1omvdco2  18498  symgsssg  18517  symggen  18520  efgval  18765  gsumzaddlem  18963  gsumconst  18976  dmdprdd  19043  dprdfeq0  19066  dprdres  19072  dprdss  19073  dprdz  19074  subgdmdprd  19078  dprddisj2  19083  dprd2dlem1  19085  dprd2da  19086  dprd2d2  19088  dmdprdsplit2lem  19089  lmhmlsp  19743  lsppratlem4  19844  islbs3  19849  lbsextlem3  19854  mplcoe5  20169  mplind  20202  znleval  20617  evpmss  20646  frlmsslsp  20856  lindff1  20880  lindfrn  20881  f1lindf  20882  lindfmm  20887  lsslindf  20890  basdif0  21477  tgcl  21493  ppttop  21531  epttop  21533  ntrin  21585  mretopd  21616  neiptoptop  21655  cnclsi  21796  cnconst2  21807  cnrest2  21810  cnpresti  21812  cnprest2  21814  fiuncmp  21928  connsub  21945  connima  21949  iunconnlem  21951  1stcfb  21969  2ndc1stc  21975  2ndcdisj  21980  kgentopon  22062  llycmpkgen2  22074  1stckgenlem  22077  kgencn3  22082  ptclsg  22139  ptcnplem  22145  txtube  22164  hausdiag  22169  txkgen  22176  xkoco1cn  22181  xkoco2cn  22182  xkococnlem  22183  qtoptop2  22223  basqtop  22235  imastopn  22244  hmeores  22295  hmphdis  22320  ptcmpfi  22337  fbssfi  22361  filin  22378  infil  22387  fgtr  22414  elfm  22471  hausflim  22505  flimclslem  22508  fclscmp  22554  cnextcn  22591  tmdgsum2  22620  tgpconncomp  22636  ustexsym  22739  ustund  22745  ustimasn  22752  utoptop  22758  utopbas  22759  restutopopn  22762  blin2  22954  metustexhalf  23081  icccmplem2  23346  icccmplem3  23347  reconnlem2  23350  tcphcph  23755  fmcfil  23790  resscdrg  23876  ivthlem2  23968  ivthlem3  23969  ivth2  23971  ovolfiniun  24017  ovoliunlem1  24018  ismbl2  24043  nulmbl2  24052  unmbl  24053  shftmbl  24054  voliunlem1  24066  voliunlem2  24067  ioombl1lem4  24077  uniioombllem4  24102  uniioombllem5  24103  dyadmbllem  24115  dyadmbl  24116  mbflimsup  24182  i1fima  24194  i1fima2  24195  i1fadd  24211  itg1addlem4  24215  itg2splitlem  24264  itg2split  24265  ellimc3  24392  limcflflem  24393  limcflf  24394  limcresi  24398  limciun  24407  dvreslem  24422  dvres2lem  24423  dvres  24424  dvaddbr  24450  dvmulbr  24451  dvlip  24505  dvlip2  24507  c1liplem1  24508  dvivthlem1  24520  dvne0  24523  lhop1lem  24525  lhop  24528  dvcnvrelem1  24529  dvcnvrelem2  24530  dvfsumle  24533  dvfsumabs  24535  dvfsumlem2  24539  itgsubstlem  24560  mdegleb  24573  mdeglt  24574  mdegldg  24575  mdegxrcl  24576  mdegcl  24578  ig1peu  24680  reeff1olem  24949  logccv  25159  rlimcnp2  25458  lgamgulmlem2  25521  ppisval  25595  prmdvdsfi  25598  mumul  25672  sqff1o  25673  chtlepsi  25696  chpub  25710  dchrisum0lem2a  26007  pntlem3  26099  ex-res  28135  htthlem  28609  chlejb1i  29168  ssmd2  30004  fz2ssnn0  30422  gsumle  30640  locfinreflem  30991  sibfof  31485  sitgclbn  31488  sitgaddlemb  31493  eulerpartlemgu  31522  ballotlemsima  31660  reprinrn  31776  bnj1311  32181  erdsze2lem2  32336  iccllysconn  32382  cvmopnlem  32410  msrf  32674  frpomin  32963  frrlem4  33011  frrlem13  33020  fprlem1  33022  frrlem15  33027  nosupno  33088  neiin  33565  neibastop1  33592  neibastop2lem  33593  topmeet  33597  poimirlem1  34761  poimirlem2  34762  poimirlem3  34763  poimirlem11  34771  poimirlem12  34772  poimirlem16  34776  poimirlem19  34779  poimirlem30  34790  cnambfre  34808  itg2gt0cn  34815  sstotbnd2  34921  sstotbnd3  34923  ssbnd  34935  ismtyima  34950  heibor1lem  34956  idresssidinxp  35435  pmodlem2  36851  pmodN  36854  diaintclN  38062  djaclN  38140  dibintclN  38171  dicval  38180  dihoml4c  38380  djhcl  38404  isnacs2  39165  isnacs3  39169  diophrw  39218  pellfundre  39340  pellfundge  39341  pellfundlb  39343  pellfundglb  39344  fnwe2lem2  39513  lmhmfgima  39546  hbt  39592  cnvtrcl0  39848  trclrelexplem  39918  relexp0a  39923  rp-imass  39979  isotone2  40261  climinf  41749  islptre  41762  limccog  41763  limcleqr  41787  itgcoscmulx  42116  ismbl3  42134  ismbl4  42141  stoweidlem27  42175  dirkercncflem2  42252  fourierdlem38  42293  fourierdlem49  42303  fourierdlem51  42305  fourierdlem54  42308  fourierdlem63  42317  fourierdlem68  42322  fourierdlem69  42323  fourierdlem70  42324  fourierdlem74  42328  fourierdlem75  42329  fourierdlem76  42330  fourierdlem80  42334  fourierdlem84  42338  fourierdlem85  42339  fourierdlem88  42342  fourierdlem100  42354  fourierdlem101  42355  fourierdlem104  42358  fourierdlem107  42361  fourierdlem111  42365  fourierdlem112  42366  caragenel2d  42677  hoidmv1lelem3  42738  hspmbllem3  42773  sssmf  42878  smfrec  42927  smfsuplem1  42948  mgmhmima  43898
  Copyright terms: Public domain W3C validator