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

Theorem ssind 3820
Description: A deduction showing that a subclass of two classes is a subclass of their intersection. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
Hypotheses
Ref Expression
ssind.1 (𝜑𝐴𝐵)
ssind.2 (𝜑𝐴𝐶)
Assertion
Ref Expression
ssind (𝜑𝐴 ⊆ (𝐵𝐶))

Proof of Theorem ssind
StepHypRef Expression
1 ssind.1 . . 3 (𝜑𝐴𝐵)
2 ssind.2 . . 3 (𝜑𝐴𝐶)
31, 2jca 554 . 2 (𝜑 → (𝐴𝐵𝐴𝐶))
4 ssin 3818 . 2 ((𝐴𝐵𝐴𝐶) ↔ 𝐴 ⊆ (𝐵𝐶))
53, 4sylib 208 1 (𝜑𝐴 ⊆ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  cin 3559  wss 3560
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-v 3193  df-in 3567  df-ss 3574
This theorem is referenced by:  mreexexlem3d  16222  isacs1i  16234  rescabs  16409  funcres2c  16477  lsmmod  18004  gsumzres  18226  gsumzsubmcl  18234  gsum2d  18287  issubdrg  18721  lspdisj  19039  mplind  19416  ntrin  20770  elcls  20782  neitr  20889  restcls  20890  lmss  21007  xkoinjcn  21395  trfg  21600  trust  21938  utoptop  21943  restutop  21946  isngp2  22306  lebnumii  22668  causs  22999  dvreslem  23574  c1lip3  23661  ssjo  28146  dmdbr5  29007  mdslj2i  29019  mdsl2bi  29022  mdslmd1lem2  29025  mdsymlem5  29106  bnj1286  30787  mclsind  31167  neiin  31961  topmeet  31993  fnemeet2  31996  bj-restpw  32674  bj-restb  32676  bj-restuni2  32680  pmod1i  34600  dihmeetlem1N  36045  dihglblem5apreN  36046  dochdmj1  36145  mapdin  36417  baerlem3lem2  36465  baerlem5alem2  36466  baerlem5blem2  36467  trrelind  37424  isotone2  37815  nzin  37985  inmap  38861  islptre  39242  limccog  39243  limcresiooub  39265  limcresioolb  39266  fourierdlem48  39665  fourierdlem49  39666  fourierdlem113  39730  pimiooltgt  40215  pimdecfgtioc  40219  pimincfltioc  40220  pimdecfgtioo  40221  pimincfltioo  40222  sssmf  40241  smflimlem2  40274  smfsuplem1  40311  setrec2fun  41706
  Copyright terms: Public domain W3C validator