Theorem abssdv 3573

Description: Deduction of abstraction subclass from implication. (Contributed by NM, 20-Jan-2006.)

Hypothesis

Ref	Expression
abssdv.1

Assertion

Ref	Expression
abssdv

Distinct variable groups:   ,   ,

Proof of Theorem abssdv

Step	Hyp	Ref	Expression
1		abssdv.1	. . 3
2	1	alrimiv 1719	. 2
3		abss 3568	. 2
4	2, 3	sylibr 212	1

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

This theorem is referenced by:  dfopif  4214  fmpt  6052  opabex2  6738  eroprf  7428  cfslb2n  8669  rankcf  9176  genpv  9398  genpdm  9401  fimaxre3  10517  supmul  10536  hashfacen  12503  hashf1lem1  12504  hashf1lem2  12505  swrd0  12658  mertenslem2  13694  4sqlem11  14473  symgbas  16405  lss1d  17609  lspsn  17648  lpval  19640  lpsscls  19642  ptuni2  20077  ptbasfi  20082  prdstopn  20129  xkopt  20156  tgpconcompeqg  20610  metrest  21027  mbfeqalem  22049  limcfval  22276  nmosetre  25679  nmopsetretALT  26782  nmfnsetre  26796  sigaclcuni  28118  deranglem  28610  derangsn  28614  liness  29795  supadd  30042  mblfinlem3  30053  ismblfin  30055  itg2addnclem  30066  areacirclem2  30108  sdclem2  30235  sdclem1  30236  ismtyval  30296  heibor1lem  30305  heibor1  30306  eldiophb  30690  hbtlem2  31073  upbdrech  31505  bnj849  33983  pmapglbx  35493

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