Theorem spv 1871

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 144	. 2 |- ( x = y -> ( ph -> ps ) )
3	2	spimv 1822	1 |- ( A. x ph -> ps )

Syntax hints:   -> wi 4   <-> wb 105   A.wal 1362

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545

This theorem depends on definitions:  df-bi 117  df-nf 1472

This theorem is referenced by:  spvv  1919  cbvalvw  1931  chvarv  1949  ru  2976  nalset  4148  tfisi  4604  tfr1onlemsucfn  6366  tfr1onlemsucaccv  6367  tfr1onlembxssdm  6369  tfr1onlembfn  6370  tfr1onlemres  6375  tfri1dALT  6377  tfrcllemsucfn  6379  tfrcllemsucaccv  6380  tfrcllembxssdm  6382  tfrcllembfn  6383  tfrcllemres  6388  findcard2  6918  findcard2s  6919  bj-nalset  15125