Theorem ss2abi 3571

Description: Inference of abstraction subclass from implication. (Contributed by NM, 31-Mar-1995.)

Hypothesis

Ref	Expression
ss2abi.1

Assertion

Ref	Expression
ss2abi

Proof of Theorem ss2abi

Step	Hyp	Ref	Expression
1		ss2ab 3567	. 2
2		ss2abi.1	. 2
3	1, 2	mpgbir 1622	1

Syntax hints:  ->wi 4  {cab 2442  C_wss 3475

This theorem is referenced by:  abssi  3574  rabssab  3586  intabs  4613  abssexg  4637  imassrn  5353  fvclss  6154  fabexg  6756  f1oabexg  6759  mapex  7445  tc2  8194  hta  8336  infmap2  8619  cflm  8651  cflim2  8664  hsmex3  8835  domtriomlem  8843  axdc3lem2  8852  brdom7disj  8930  brdom6disj  8931  npex  9385  hashf1lem2  12505  issubc  15204  isghm  16267  symgbasfi  16411  tgval  19456  ustfn  20704  ustval  20705  ustn0  20723  birthdaylem1  23281  wlks  24519  trls  24538  mptctf  27544  measbase  28168  measval  28169  ismeas  28170  isrnmeas  28171  ballotlem2  28427  subfaclefac  28620  dfon2lem2  29216  sdclem2  30235  eldiophb  30690  hbtlem1  31072  hbtlem7  31074  rabexgf  31399  relopabVD  33701  lineset  35462  lautset  35806  pautsetN  35822  tendoset  36485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-in 3482  df-ss 3489