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

Theorem sstrdi 3957
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 3955 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3911
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3448  df-in 3918  df-ss 3928
This theorem is referenced by:  difss2  4094  rintn0  5070  eqbrrdva  5826  ssxpb  6127  resssxp  6223  relfld  6228  funssxp  6698  dff2  7050  dff3  7051  fliftf  7261  1stcof  7952  2ndcof  7953  frxp2  8077  frxp3  8084  frrlem13  8230  nnunifi  9239  elfiun  9367  marypha1lem  9370  marypha1  9371  ordtypelem7  9461  tcmin  9678  unwf  9747  rankfu  9814  tcrank  9821  aceq3lem  10057  dfac12lem2  10081  ackbij1lem9  10165  ackbij1lem10  10166  ackbij1lem16  10172  fin23lem26  10262  fin23lem27  10265  fin1a2lem6  10342  itunitc  10358  axdc3lem2  10388  ttukeylem5  10450  fpwwe2lem12  10579  canthwelem  10587  pwfseqlem4  10599  wunex2  10675  wunex3  10678  inar1  10712  inatsk  10715  gruina  10755  suprfinzcl  12618  suprzub  12865  uzsupss  12866  uzwo3  12869  rpnnen1lem4  12906  rpnnen1lem5  12907  supxrre  13247  infxrre  13256  ioodisj  13400  supicclub2  13422  fzssnn  13486  fzossnn0  13604  elfzom1elp1fzo  13640  injresinjlem  13693  uzindi  13888  ssnn0fi  13891  seqcoll  14364  seqcoll2  14365  reltrclfv  14903  relexpdmg  14928  relexpdm  14929  relexprng  14932  relexprn  14933  relexpfld  14935  relexpaddg  14939  limsupval2  15363  limsupgre  15364  limsupbnd2  15366  rlimuni  15433  rlimcld2  15461  rlimno1  15539  isercolllem2  15551  isercoll  15553  summolem2a  15601  summolem2  15602  fsumsers  15614  fsumcvg3  15615  prodmolem2a  15818  prodmolem2  15819  zprod  15821  lcmfnnval  16501  lcmfnncl  16506  4sqlem11  16828  vdwlem8  16861  vdwlem11  16864  ramub2  16887  0ram  16893  0ram2  16894  0ramcl  16896  ramub1lem2  16900  prmgaplem3  16926  prmgaplem4  16927  isohom  17660  funcres2c  17789  resscntz  19113  cntzidss  19119  cntzmhm2  19121  pgpssslw  19397  cntzspan  19623  gsumval3  19685  gsum2d  19750  dprdspan  19807  dprdres  19808  subdrgint  20273  sdrgint  20274  primefld  20275  lssintcl  20428  lbsextlem2  20623  lbsextlem3  20624  lbsextlem4  20625  islinds3  21243  fctop  22357  cctop  22359  neitr  22534  ordtbas2  22545  ordtopn1  22548  ordtopn2  22549  lmss  22652  clsconn  22784  2ndcdisj  22810  2ndcomap  22812  ptbasfi  22935  txcmplem2  22996  hausdiag  22999  txkgen  23006  basqtop  23065  alexsubb  23400  alexsubALTlem4  23404  tsmsres  23498  tsmsxplem1  23507  tsmsxp  23509  ustrel  23566  utop3cls  23606  prdsmet  23726  metustrel  23911  icccmplem2  24189  xrge0tsms  24200  cnmptre  24293  icchmeo  24307  bndth  24324  lebnumlem2  24328  cfilresi  24662  causs  24665  bcthlem5  24695  evthicc  24826  ovolficcss  24836  ovolmge0  24844  ovolgelb  24847  ovollb2lem  24855  ovollb2  24856  ovolunlem1a  24863  ovolunlem1  24864  ovoliunlem1  24869  ovoliunlem2  24870  ovoliun  24872  ovolscalem1  24880  ovolicc1  24883  ovolicc2lem4  24887  ovolicc2  24889  voliunlem2  24918  voliunlem3  24919  ioombl1lem2  24926  ioombl1lem4  24928  uniioovol  24946  uniiccvol  24947  uniioombllem1  24948  uniioombllem2  24950  uniioombllem3  24952  uniioombllem4  24953  uniioombllem6  24955  dyadmbllem  24966  dyadmbl  24967  volcn  24973  vitalilem4  24978  vitalilem5  24979  cnmbf  25026  i1fmul  25063  itg1addlem4  25066  itg1addlem4OLD  25067  itg2seq  25110  dvbssntr  25267  dvreslem  25276  dvcjbr  25316  dvferm1  25352  dvferm2  25354  cmvth  25358  dvlip  25360  lhop1lem  25380  lhop2  25382  lhop  25383  dvcnvrelem2  25385  dvcnvre  25386  dvfsumle  25388  dvfsumge  25389  dvfsumabs  25390  dvfsumlem2  25394  ftc1a  25404  ftc1lem3  25405  ftc1lem6  25408  itgsubstlem  25415  itgpowd  25417  mdegleb  25432  mdeglt  25433  mdegldg  25434  mdegxrcl  25435  mdegcl  25437  deg1mul3le  25484  ig1pdvds  25544  plyeq0lem  25574  aannenlem2  25692  aalioulem3  25697  taylf  25723  taylthlem2  25736  pserulm  25784  psercn2  25785  psercn  25788  reeff1olem  25808  efcvx  25811  loglesqrt  26114  rlimcnp  26318  xrlimcnp  26321  jensen  26341  wilthlem2  26421  vmadivsumb  26834  pntrsumo1  26916  pntlem3  26960  perpln2  27656  axcontlem10  27925  usgrexmplef  28210  nmoxr  29711  nmooge0  29712  nmoolb  29716  nmoubi  29717  ubthlem1  29815  shmodi  30335  nmopxr  30811  nmfnxr  30824  nmoplb  30852  nmopub  30853  nmfnlb  30869  nmfnleub  30870  nmopun  30959  branmfn  31050  mdslj1i  31264  hatomistici  31307  xppreima2  31570  fsuppcurry1  31645  fsuppcurry2  31646  fpwrelmap  31653  infxrge0gelb  31674  prmdvdsbc  31715  gsumpart  31900  xrge0tsmsd  31902  pmtrcnel2  31944  cyc3genpm  32004  1fldgenq  32092  ssmxidllem  32241  zarcmplem  32465  metideq  32477  metider  32478  pstmfval  32480  esumgect  32692  esum2d  32695  sigaclci  32734  insiga  32739  omssubadd  32903  eulerpartlemgs2  32983  ballotlemsima  33118  signsply0  33166  iblidicc  33208  fsum2dsub  33223  reprsuc  33231  reprgt  33237  bnj1145  33608  bnj1137  33610  bnj1136  33612  resconn  33843  cvmliftlem8  33889  cvmlift3lem6  33921  mclsssvlem  34159  mclsind  34167  mclsppslem  34180  ivthALT  34810  neibastop1  34834  topjoin  34840  bj-imdirco  35664  ptrecube  36081  poimirlem6  36087  poimirlem15  36096  heicant  36116  mblfinlem2  36119  mblfinlem3  36120  mblfinlem4  36121  ismblfin  36122  itg2gt0cn  36136  ftc1cnnc  36153  ftc1anclem3  36156  ftc1anclem7  36160  ftc1anclem8  36161  ftc1anc  36162  areacirclem2  36170  areacirclem3  36171  areacirclem4  36172  totbndbnd  36251  prdsbnd  36255  heiborlem1  36273  rrnequiv  36297  reheibor  36301  iccbnd  36302  pmapssbaN  38226  2polssN  38381  paddunN  38393  poldmj1N  38394  ispsubcl2N  38413  psubclinN  38414  paddatclN  38415  poml4N  38419  diaglbN  39521  diaintclN  39524  dibglbN  39632  dibintclN  39633  dicssdvh  39652  dihvalrel  39745  dochexmidlem4  39929  infdesc  40984  rmxyelqirrOLD  41237  ttac  41363  hbtlem6  41459  hbt  41460  cnvssb  41865  cnvrcl0  41904  cnvtrrel  41949  relexpaddss  41997  cotrcltrcl  42004  cotrclrcl  42021  frege96d  42028  frege97d  42031  frege109d  42036  frege131d  42043  rfovcnvf1od  42283  isotone2  42328  gneispace  42413  k0004ss1  42430  grumnudlem  42572  uzfissfz  43567  suplesup  43580  ssrexr  43674  limciccioolb  43869  limcicciooub  43885  limcleqr  43892  cnrefiisplem  44077  cncfiooicclem1  44141  ibliccsinexp  44199  iblioosinexp  44201  itgcoscmulx  44217  itgsincmulx  44222  itgsubsticclem  44223  itgiccshift  44228  itgperiod  44229  itgsbtaddcnst  44230  stoweidlem34  44282  stoweidlem59  44307  dirkeritg  44350  dirkercncflem2  44352  fourierdlem20  44375  fourierdlem31  44386  fourierdlem39  44394  fourierdlem42  44397  fourierdlem46  44400  fourierdlem52  44406  fourierdlem53  44407  fourierdlem60  44414  fourierdlem61  44415  fourierdlem62  44416  fourierdlem68  44422  fourierdlem76  44430  fourierdlem85  44439  fourierdlem88  44442  fourierdlem89  44443  fourierdlem90  44444  fourierdlem91  44445  fourierdlem93  44447  fourierdlem94  44448  fourierdlem103  44457  fourierdlem104  44458  fourierdlem111  44465  fouriersw  44479  etransclem46  44528  etransclem48  44530  sge0less  44640  sge0resplit  44654  sge0isum  44675  pimdecfgtioo  44965  pimincfltioo  44966  iccpartipre  45620  bgoldbtbndlem2  46005  setrec1lem4  47142  setrec2fun  47144
  Copyright terms: Public domain W3C validator