Theorem spv 2260

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

Hypothesis

Ref	Expression
spv.1	|- ( x = y -> ( ph <-> ps ) )

Assertion

Ref	Expression
spv	|- ( A. x ph -> ps )

Distinct variable group:   ps, x

Allowed substitution hints:   ph( x, y)   ps( y)

Proof of Theorem spv

Step	Hyp	Ref	Expression
1		spv.1	. . 3 |- ( x = y -> ( ph <-> ps ) )
2	1	biimpd 219	. 2 |- ( x = y -> ( ph -> ps ) )
3	2	spimv 2257	1 |- ( A. x ph -> ps )

Syntax hints:   -> wi 4   <-> wb 196   A.wal 1481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-12 2047  ax-13 2246

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705

This theorem is referenced by:  chvarv  2263  cbvalv  2273  ru  3434  nalset  4795  isowe2  6600  tfisi  7058  findcard2  8200  marypha1lem  8339  setind  8610  karden  8758  kmlem4  8975  axgroth3  9653  ramcl  15733  alexsubALTlem3  21853  i1fd  23448  dfpo2  31645  dfon2lem6  31693  trer  32310  axc11n-16  34223  elsetrecslem  42444