Theorem ss2abdv 3572

Description: Deduction of abstraction subclass from implication. (Contributed by NM, 29-Jul-2011.)

Hypothesis

Ref	Expression
ss2abdv.1

Assertion

Ref	Expression
ss2abdv

Distinct variable group:   ,

Proof of Theorem ss2abdv

Step	Hyp	Ref	Expression
1		ss2abdv.1	. . 3
2	1	alrimiv 1719	. 2
3		ss2ab 3567	. 2
4	2, 3	sylibr 212	1

Syntax hints:  ->wi 4  A.wal 1393  {cab 2442  C_wss 3475

This theorem is referenced by:  intss  4307  ssopab2  4778  opabbrexOLD  6340  ssoprab2  6353  suppimacnvss  6928  suppimacnv  6929  ressuppss  6938  ss2ixp  7502  fiss  7904  tcss  8196  tcel  8197  infmap2  8619  cfub  8650  cflm  8651  cflecard  8654  cncmet  21761  plyss  22596  ofrn2  27480  sigaclci  28132  subfacp1lem6  28629  ss2mcls  28928  itg2addnclem  30066  sdclem1  30236  istotbnd3  30267  sstotbnd  30271  aomclem4  31003  hbtlem4  31075  hbtlem3  31076  rngunsnply  31122  iocinico  31179

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