Theorem spv 1874

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 1825	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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548

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

This theorem is referenced by:  spvv  1922  cbvalvw  1934  chvarv  1956  ru  2988  nalset  4164  tfisi  4624  tfr1onlemsucfn  6400  tfr1onlemsucaccv  6401  tfr1onlembxssdm  6403  tfr1onlembfn  6404  tfr1onlemres  6409  tfri1dALT  6411  tfrcllemsucfn  6413  tfrcllemsucaccv  6414  tfrcllembxssdm  6416  tfrcllembfn  6417  tfrcllemres  6422  findcard2  6952  findcard2s  6953  bj-nalset  15567