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

Theorem syl5sseqr 3449
Description: Subclass transitivity deduction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
Hypotheses
Ref Expression
syl5sseqr.1  |-  B  C_  A
syl5sseqr.2  |-  ( ph  ->  C  =  A )
Assertion
Ref Expression
syl5sseqr  |-  ( ph  ->  B  C_  C )

Proof of Theorem syl5sseqr
StepHypRef Expression
1 syl5sseqr.1 . . 3  |-  B  C_  A
21a1i 11 . 2  |-  ( ph  ->  B  C_  A )
3 syl5sseqr.2 . 2  |-  ( ph  ->  C  =  A )
42, 3sseqtr4d 3437 1  |-  ( ph  ->  B  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1448    C_ wss 3372
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1673  ax-4 1686  ax-5 1762  ax-6 1809  ax-7 1855  ax-10 1919  ax-11 1924  ax-12 1937  ax-13 2092  ax-ext 2432
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1451  df-ex 1668  df-nf 1672  df-sb 1802  df-clab 2439  df-cleq 2445  df-clel 2448  df-in 3379  df-ss 3386
This theorem is referenced by:  unissint  4229  resdif  5817  fimacnv  5996  tfrlem5  7085  domss2  7718  dffi3  7932  cantnfp1lem3  8172  trcl  8199  tcid  8210  r1ordg  8236  r1sssuc  8241  ackbij1lem15  8651  cfsmolem  8687  isfin4-3  8732  fin1a2lem7  8823  wunex2  9150  wuncid  9155  trclfvlb  13083  rtrclreclem1  13132  fsumsplit  13817  o1fsum  13884  fprodsplit  14031  phimullem  14738  vdwlem6  14947  ressinbas  15196  mrcssid  15534  mreexexlem2d  15562  acsfiindd  16434  dirge  16494  symgbasfi  17038  efgredlemf  17402  efgredlemd  17405  gsumzres  17554  gsumzcl2  17555  gsumzf1o  17557  gsumadd  17567  gsumzsplit  17571  gsumsplit2  17573  dprd2da  17686  dmdprdsplit2lem  17689  dmdprdsplit2  17690  dmdprdsplit  17691  dprdsplit  17692  invrpropd  17937  issubdrg  18044  lspssid  18219  aspssid  18568  pjcss  19290  istopon  19951  sscls  20082  ordtbas  20219  cncls2  20300  tgcmp  20427  cmpfi  20434  1stcfb  20471  1stckgenlem  20579  ptbasfi  20607  ptcnplem  20647  ptuncnv  20833  ptunhmeo  20834  fbasrn  20910  cnflf2  21029  fclscmp  21056  alexsublem  21070  ghmcnp  21140  tsmsgsum  21164  tsmsres  21169  tsmssplit  21177  tsmsxplem1  21178  ustssco  21240  mopnfss  21469  cnmpt2pc  21967  uniiccdif  22547  uniioombllem3  22555  uniioombllem4  22556  itg2splitlem  22718  itg2split  22719  itgsplit  22805  ellimc2  22844  ellimc3  22846  lhop  22980  plyaddlem1  23179  plymullem1  23180  taylthlem2  23341  mtest  23371  xrlimcnp  23906  fsumharmonic  23949  chtdif  24097  dchrghm  24196  lgsquadlem2  24295  dchrisumlema  24338  dchrisumlem2  24340  dchrisum0lem1b  24365  dchrisum0lem1  24366  pntrlog2bndlem6  24433  pntlemf  24455  ex-res  25903  spanss2  27010  mdsymi  28076  padct  28315  ordtconlem1  28737  issgon  28952  sssigagen  28974  measiuns  29046  sitgclg  29181  cvmliftlem10  30023  ftc1anclem6  32024  heibor1lem  32143  heibor  32155  divrngcl  32198  isdrngo2  32199  igenss  32297  paddunssN  33375  sspadd1  33382  sspadd2  33383  pclssidN  33462  diassdvaN  34630  dochvalr  34927  lcdvbase  35163  nacsfix  35556  isnumbasgrplem2  35965  rgspnssid  36038  itgpowd  36101  trrelsuperrel2dg  36265  fvilbd  36283  relexp0a  36310  wnefimgd  36602  icccncfext  37807  iblsplit  37885  dirkeritg  38021  dirkercncflem2  38023  fourierdlem81  38108  fourierdlem89  38116  fourierdlem91  38118  fourierdlem92  38119  fourierdlem111  38138  fouriercn  38153  hspdifhsp  38501  umgr2adedgwlk  39946  umgr2adedgwlkon  39947  umgr2adedgspth  39949  srhmsubc  40403  srhmsubcALTV  40422  gsumsplit2f  40471  fdivmpt  40676  fdivpm  40679  refdivpm  40680
  Copyright terms: Public domain W3C validator