Theorem spv 1847

Description: Specialization, using implicit substitition. (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 143	. 2 |- ( x = y -> ( ph -> ps ) )
3	2	spimv 1798	1 |- ( A. x ph -> ps )

Syntax hints:   -> wi 4   <-> wb 104   A.wal 1340

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1434  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521

This theorem depends on definitions:  df-bi 116  df-nf 1448

This theorem is referenced by:  spvv  1894  cbvalvw  1906  chvarv  1924  ru  2945  nalset  4106  tfisi  4558  tfr1onlemsucfn  6299  tfr1onlemsucaccv  6300  tfr1onlembxssdm  6302  tfr1onlembfn  6303  tfr1onlemres  6308  tfri1dALT  6310  tfrcllemsucfn  6312  tfrcllemsucaccv  6313  tfrcllembxssdm  6315  tfrcllembfn  6316  tfrcllemres  6321  findcard2  6846  findcard2s  6847  bj-nalset  13612