Theorem spv 2011

Description: Specialization, using implicit substitution. (Contributed by NM, 30-Aug-1993.)

Hypothesis

Ref	Expression
spv.1

Assertion

Ref	Expression
spv

Distinct variable group:   ,

Proof of Theorem spv

Step	Hyp	Ref	Expression
1		spv.1	. . 3
2	1	biimpd 207	. 2
3	2	spimv 2009	1

Syntax hints:  ->wi 4  <->wb 184  A.wal 1393

This theorem is referenced by:  axc11n-16  2268  ru  3326  nalset  4589  isowe2  6246  tfisi  6693  findcard2  7780  marypha1lem  7913  setind  8186  karden  8334  kmlem4  8554  axgroth3  9230  ramcl  14547  alexsubALTlem3  20549  i1fd  22088  dfpo2  29184  dfon2lem6  29220  trer  30134

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-12 1854  ax-13 1999

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-nf 1617