ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  sselid GIF version

Theorem sselid 3145
Description: Membership inference from subclass relationship. (Contributed by NM, 25-Jun-2014.)
Hypotheses
Ref Expression
sseli.1 𝐴𝐵
sselid.2 (𝜑𝐶𝐴)
Assertion
Ref Expression
sselid (𝜑𝐶𝐵)

Proof of Theorem sselid
StepHypRef Expression
1 sselid.2 . 2 (𝜑𝐶𝐴)
2 sseli.1 . . 3 𝐴𝐵
32sseli 3143 . 2 (𝐶𝐴𝐶𝐵)
41, 3syl 14 1 (𝜑𝐶𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 2141  wss 3121
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152
This theorem depends on definitions:  df-bi 116  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-in 3127  df-ss 3134
This theorem is referenced by:  mptrcl  5576  riotacl  5820  riotasbc  5821  elmpocl  6044  ofrval  6068  f1od2  6211  mpoxopn0yelv  6215  tpostpos  6240  smores  6268  supubti  6972  suplubti  6973  prarloclemcalc  7451  rereceu  7838  recriota  7839  rexrd  7956  eqord1  8389  nnred  8878  nncnd  8879  un0addcl  9155  un0mulcl  9156  nnnn0d  9175  nn0red  9176  nn0xnn0d  9194  suprzclex  9297  nn0zd  9319  zred  9321  rpred  9640  ige2m1fz  10053  zmodfzp1  10291  seq3caopr2  10425  expcl2lemap  10475  m1expcl  10486  summodclem2a  11331  zsumdc  11334  clim2prod  11489  ntrivcvgap  11498  prodmodclem2a  11526  zproddc  11529  zsupssdc  11896  lcmn0cl  12009  isprm5lem  12082  eulerthlemrprm  12170  eulerthlema  12171  eulerthlemh  12172  eulerthlemth  12173  prmdivdiv  12178  ennnfonelemg  12345  lmrcl  12944  lmss  12999  upxp  13025  isxms2  13205  iooretopg  13281  tgqioo  13300  limccoap  13400  dvcl  13405  dvidlemap  13413  dvcnp2cntop  13416  lgscl  13668  2sqlem6  13709  2sqlem8  13712  2sqlem9  13713  isomninnlem  14022  trilpolemeq1  14032  trilpolemlt1  14033  iswomninnlem  14041  iswomni0  14043  ismkvnnlem  14044  nconstwlpolemgt0  14055
  Copyright terms: Public domain W3C validator