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

Theorem sstrdi 3954
Description: Subclass transitivity deduction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
Hypotheses
Ref Expression
sstrdi.1 (𝜑𝐴𝐵)
sstrdi.2 𝐵𝐶
Assertion
Ref Expression
sstrdi (𝜑𝐴𝐶)

Proof of Theorem sstrdi
StepHypRef Expression
1 sstrdi.1 . 2 (𝜑𝐴𝐵)
2 sstrdi.2 . . 3 𝐵𝐶
32a1i 11 . 2 (𝜑𝐵𝐶)
41, 3sstrd 3952 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3909
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-12 2177  ax-ext 2792
This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-sb 2070  df-clab 2799  df-cleq 2813  df-clel 2891  df-v 3472  df-in 3916  df-ss 3926
This theorem is referenced by:  difss2  4085  rintn0  5002  eqbrrdva  5712  ssxpb  6003  relfld  6098  funssxp  6507  dff2  6837  dff3  6838  fliftf  7041  1stcof  7693  2ndcof  7694  nnunifi  8743  elfiun  8868  marypha1lem  8871  marypha1  8872  ordtypelem7  8962  tcmin  9157  unwf  9213  rankfu  9280  tcrank  9287  aceq3lem  9520  dfac12lem2  9544  ackbij1lem9  9624  ackbij1lem10  9625  ackbij1lem16  9631  fin23lem26  9721  fin23lem27  9724  fin1a2lem6  9801  itunitc  9817  axdc3lem2  9847  ttukeylem5  9909  fpwwe2lem13  10038  canthwelem  10046  pwfseqlem4  10058  wunex2  10134  wunex3  10137  inar1  10171  inatsk  10174  gruina  10214  suprfinzcl  12072  suprzub  12314  uzsupss  12315  uzwo3  12318  rpnnen1lem4  12354  rpnnen1lem5  12355  supxrre  12695  infxrre  12704  ioodisj  12847  supicclub2  12869  fzssnn  12931  fzossnn0  13048  elfzom1elp1fzo  13084  injresinjlem  13137  uzindi  13330  ssnn0fi  13333  seqcoll  13803  seqcoll2  13804  reltrclfv  14353  relexpdmg  14377  relexpdm  14378  relexprng  14381  relexprn  14382  relexpfld  14384  relexpaddg  14388  limsupval2  14813  limsupgre  14814  limsupbnd2  14816  rlimuni  14883  rlimcld2  14911  rlimno1  14986  isercolllem2  14998  isercoll  15000  summolem2a  15048  summolem2  15049  fsumsers  15061  fsumcvg3  15062  prodmolem2a  15264  prodmolem2  15265  zprod  15267  lcmfnnval  15942  lcmfnncl  15947  4sqlem11  16265  vdwlem8  16298  vdwlem11  16301  ramub2  16324  0ram  16330  0ram2  16331  0ramcl  16333  ramub1lem2  16337  prmgaplem3  16363  prmgaplem4  16364  isohom  17021  funcres2c  17146  resscntz  18437  cntzidss  18443  cntzmhm2  18445  pgpssslw  18714  cntzspan  18939  gsumval3  19002  gsum2d  19067  dprdspan  19124  dprdres  19125  subdrgint  19554  sdrgint  19555  primefld  19556  lssintcl  19708  lbsextlem2  19903  lbsextlem3  19904  lbsextlem4  19905  islinds3  20950  fctop  21584  cctop  21586  neitr  21760  ordtbas2  21771  ordtopn1  21774  ordtopn2  21775  lmss  21878  clsconn  22010  2ndcdisj  22036  2ndcomap  22038  ptbasfi  22161  txcmplem2  22222  hausdiag  22225  txkgen  22232  basqtop  22291  alexsubb  22626  alexsubALTlem4  22630  tsmsres  22724  tsmsxplem1  22733  tsmsxp  22735  ustrel  22792  utop3cls  22832  prdsmet  22952  metustrel  23134  icccmplem2  23403  xrge0tsms  23414  cnmptre  23507  icchmeo  23521  bndth  23538  lebnumlem2  23542  cfilresi  23874  causs  23877  bcthlem5  23907  evthicc  24038  ovolficcss  24048  ovolmge0  24056  ovolgelb  24059  ovollb2lem  24067  ovollb2  24068  ovolunlem1a  24075  ovolunlem1  24076  ovoliunlem1  24081  ovoliunlem2  24082  ovoliun  24084  ovolscalem1  24092  ovolicc1  24095  ovolicc2lem4  24099  ovolicc2  24101  voliunlem2  24130  voliunlem3  24131  ioombl1lem2  24138  ioombl1lem4  24140  uniioovol  24158  uniiccvol  24159  uniioombllem1  24160  uniioombllem2  24162  uniioombllem3  24164  uniioombllem4  24165  uniioombllem6  24167  dyadmbllem  24178  dyadmbl  24179  volcn  24185  vitalilem4  24190  vitalilem5  24191  cnmbf  24238  i1fmul  24275  itg1addlem4  24278  itg2seq  24321  dvbssntr  24478  dvreslem  24487  dvcjbr  24527  dvferm1  24563  dvferm2  24565  cmvth  24569  dvlip  24571  lhop1lem  24591  lhop2  24593  lhop  24594  dvcnvrelem2  24596  dvcnvre  24597  dvfsumle  24599  dvfsumge  24600  dvfsumabs  24601  dvfsumlem2  24605  ftc1a  24615  ftc1lem3  24616  ftc1lem6  24619  itgsubstlem  24626  itgpowd  24628  mdegleb  24640  mdeglt  24641  mdegldg  24642  mdegxrcl  24643  mdegcl  24645  deg1mul3le  24692  ig1pdvds  24752  plyeq0lem  24782  aannenlem2  24900  aalioulem3  24905  taylf  24931  taylthlem2  24944  pserulm  24992  psercn2  24993  psercn  24996  reeff1olem  25016  efcvx  25019  loglesqrt  25322  rlimcnp  25526  xrlimcnp  25529  jensen  25549  wilthlem2  25629  vmadivsumb  26042  pntrsumo1  26124  pntlem3  26168  perpln2  26480  axcontlem10  26742  usgrexmplef  27024  nmoxr  28524  nmooge0  28525  nmoolb  28529  nmoubi  28530  ubthlem1  28628  shmodi  29148  nmopxr  29624  nmfnxr  29637  nmoplb  29665  nmopub  29666  nmfnlb  29682  nmfnleub  29683  nmopun  29772  branmfn  29863  mdslj1i  30077  hatomistici  30120  xppreima2  30378  fsuppcurry1  30444  fsuppcurry2  30445  fpwrelmap  30452  infxrge0gelb  30473  prmdvdsbc  30515  xrge0tsmsd  30696  pmtrcnel2  30738  cyc3genpm  30798  ssmxidllem  30985  metideq  31140  metider  31141  pstmfval  31143  esumgect  31353  esum2d  31356  sigaclci  31395  insiga  31400  omssubadd  31562  eulerpartlemgs2  31642  ballotlemsima  31777  signsply0  31825  iblidicc  31867  fsum2dsub  31882  reprsuc  31890  reprgt  31896  bnj1145  32269  bnj1137  32271  bnj1136  32273  resconn  32497  cvmliftlem8  32543  cvmlift3lem6  32575  mclsssvlem  32813  mclsind  32821  mclsppslem  32834  frrlem13  33139  nosupbday  33209  ivthALT  33687  neibastop1  33711  topjoin  33717  ptrecube  34929  poimirlem6  34935  poimirlem15  34944  heicant  34964  mblfinlem2  34967  mblfinlem3  34968  mblfinlem4  34969  ismblfin  34970  itg2gt0cn  34984  ftc1cnnc  35001  ftc1anclem3  35004  ftc1anclem7  35008  ftc1anclem8  35009  ftc1anc  35010  areacirclem2  35018  areacirclem3  35019  areacirclem4  35020  totbndbnd  35099  prdsbnd  35103  heiborlem1  35121  rrnequiv  35145  reheibor  35149  iccbnd  35150  pmapssbaN  36928  2polssN  37083  paddunN  37095  poldmj1N  37096  ispsubcl2N  37115  psubclinN  37116  paddatclN  37117  poml4N  37121  diaglbN  38223  diaintclN  38226  dibglbN  38334  dibintclN  38335  dicssdvh  38354  dihvalrel  38447  dochexmidlem4  38631  rmxyelqirr  39640  ttac  39766  hbtlem6  39862  hbt  39863  cnvssb  40077  cnvrcl0  40116  cnvtrrel  40146  relexpaddss  40194  cotrcltrcl  40201  cotrclrcl  40218  frege96d  40225  frege97d  40228  frege109d  40233  frege131d  40240  rp-imass  40248  rfovcnvf1od  40481  isotone2  40530  gneispace  40615  k0004ss1  40632  grumnudlem  40772  uzfissfz  41744  suplesup  41757  ssrexr  41856  limciccioolb  42050  limcicciooub  42066  limcleqr  42073  cnrefiisplem  42258  cncfiooicclem1  42322  ibliccsinexp  42380  iblioosinexp  42382  itgcoscmulx  42398  itgsincmulx  42403  itgsubsticclem  42404  itgiccshift  42409  itgperiod  42410  itgsbtaddcnst  42411  stoweidlem34  42463  stoweidlem59  42488  dirkeritg  42531  dirkercncflem2  42533  fourierdlem20  42556  fourierdlem31  42567  fourierdlem39  42575  fourierdlem42  42578  fourierdlem46  42581  fourierdlem52  42587  fourierdlem53  42588  fourierdlem60  42595  fourierdlem61  42596  fourierdlem62  42597  fourierdlem68  42603  fourierdlem76  42611  fourierdlem85  42620  fourierdlem88  42623  fourierdlem89  42624  fourierdlem90  42625  fourierdlem91  42626  fourierdlem93  42628  fourierdlem94  42629  fourierdlem103  42638  fourierdlem104  42639  fourierdlem111  42646  fouriersw  42660  etransclem46  42709  etransclem48  42711  sge0less  42818  sge0resplit  42832  sge0isum  42853  pimdecfgtioo  43139  pimincfltioo  43140  iccpartipre  43725  bgoldbtbndlem2  44112  setrec1lem4  44976  setrec2fun  44978
  Copyright terms: Public domain W3C validator