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

Theorem sseqtrrdi 4018
Description: A chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.)
Hypotheses
Ref Expression
sseqtrrdi.1 (𝜑𝐴𝐵)
sseqtrrdi.2 𝐶 = 𝐵
Assertion
Ref Expression
sseqtrrdi (𝜑𝐴𝐶)

Proof of Theorem sseqtrrdi
StepHypRef Expression
1 sseqtrrdi.1 . 2 (𝜑𝐴𝐵)
2 sseqtrrdi.2 . . 3 𝐶 = 𝐵
32eqcomi 2830 . 2 𝐵 = 𝐶
41, 3sseqtrdi 4017 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1533  wss 3936
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-in 3943  df-ss 3952
This theorem is referenced by:  disjxiun  5056  knatar  7104  iunpw  7487  fviunfun  7640  wfrdmcl  7957  wfrlem12  7960  wfrlem16  7964  wfrlem17  7965  tfrlem9  8015  tfrlem9a  8016  tfrlem13  8020  tz7.44-2  8037  tz7.44-3  8038  tz7.49  8075  marypha1lem  8891  ordtypelem2  8977  ixpiunwdom  9049  oemapvali  9141  tcss  9180  tcel  9181  pwwf  9230  rankpwi  9246  rankval3b  9249  cplem1  9312  dfac12lem2  9564  infmap2  9634  ackbij1b  9655  ttukeylem6  9930  fpwwe2lem11  10056  fpwwe2lem12  10057  fpwwe2lem13  10058  fpwwe2  10059  uznnssnn  12289  pfxccatpfx2  14093  shftfval  14423  rexuzre  14706  climsup  15020  clim2prod  15238  fprodntriv  15290  eulerthlem2  16113  ramtlecl  16330  mreexexlem4d  16912  mreexdomd  16914  gsumpropd2lem  17883  gsumzaddlem  19035  gsum2d  19086  telgsums  19107  pgpfac1lem1  19190  pgpfac1lem3a  19192  pgpfac1lem3  19193  pgpfac1lem5  19195  lspsolvlem  19908  lbsextlem2  19925  dsmmacl  20879  eltopss  21509  difopn  21636  tgrest  21761  perfopn  21787  pnfnei  21822  mnfnei  21823  regsep2  21978  cncmp  21994  uncmp  22005  hauscmplem  22008  hauscmp  22009  conndisj  22018  cnconn  22024  conncompss  22035  2ndcctbss  22057  islly2  22086  comppfsc  22134  1stckgenlem  22155  txuni2  22167  ptbasfi  22183  ptpjopn  22214  txindis  22236  txtube  22242  hausdiag  22247  xkoinjcn  22289  tgqtop  22314  filconn  22485  elfm2  22550  flimclslem  22586  flffbas  22597  fclsbas  22623  flimfnfcls  22630  alexsubALT  22653  symgtgp  22708  ustssco  22817  isucn2  22882  ucnima  22884  ucnprima  22885  blcls  23110  prdsxmslem2  23133  isngp2  23200  tgioo  23398  xrtgioo  23408  xrsmopn  23414  opnreen  23433  cnheiborlem  23552  cnllycmp  23554  tcphcph  23834  rrxmvallem  24001  uniioombllem4  24181  dyadmbllem  24194  opnmbllem  24196  mbfimaopnlem  24250  mbflimsup  24261  i1fadd  24290  i1fmul  24291  itg1addlem4  24294  i1fmulc  24298  limciun  24486  dvlip2  24586  c1lip3  24590  lhop  24607  dvfsumlem2  24618  dvfsumrlimge0  24621  dvfsumrlim2  24623  ulmval  24962  psercnlem2  25006  efopnlem2  25234  efopn  25235  umgrres1lem  27086  upgrres1  27089  nbgrssvwo2  27138  ubthlem1  28641  issh2  28980  mdsymlem1  30174  padct  30449  xrofsup  30486  fz2ssnn0  30502  tpr2rico  31150  sibfinima  31592  fct2relem  31863  bnj906  32197  bnj1014  32228  bnj1286  32286  bnj1408  32303  bnj1450  32317  bnj1452  32319  bnj1498  32328  bnj1501  32334  lfuhgr  32359  cvmopnlem  32520  cvmfolem  32521  cvmliftlem6  32532  cvmliftlem8  32534  cvmliftlem13  32538  cvmliftlem15  32540  cvmlift2lem9  32553  cvmlift2lem11  32555  cvmlift2lem12  32556  mclsppslem  32825  trpredpred  33062  trpredtr  33064  trpredrec  33072  frrlem8  33125  frrlem10  33127  frrlem12  33129  frrlem14  33131  filnetlem4  33724  dissneqlem  34615  pibt2  34692  lindsdom  34880  opnmbllem0  34922  cnambfre  34934  heibor1lem  35081  osumcllem1N  37086  osumcllem2N  37087  pexmidlem6N  37105  dochexmidlem6  38595  dochexmidlem7  38596  mapdrvallem3  38776  k0004ss2  40495  cpcolld  40587  dvsconst  40655  dvsid  40656  dvsef  40657  iunconnlem2  41262  uzssd2  41683  climinf  41879  climsuse  41881  climresmpt  41932  climleltrp  41949  stoweidlem28  42306  stoweidlem50  42328  stoweidlem52  42330  stoweidlem53  42331  stoweidlem54  42332  fourierdlem54  42438  fourierdlem80  42464  meaiininclem  42761  caratheodorylem2  42802  hspmbllem2  42902  mbfresmf  43009  smfmbfcex  43029  smflimlem2  43041  smflimsuplem2  43088  smflimsuplem3  43089  smflimsuplem5  43091  smflimsuplem6  43092  isomuspgrlem2c  43988  upgredgssspr  44011  setrec1  44787  setrecsres  44797  aacllem  44895
  Copyright terms: Public domain W3C validator