Theorem spv 1783

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

Syntax hints:   -> wi 4   <-> wb 103   A.wal 1283

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468

This theorem depends on definitions:  df-bi 115  df-nf 1391

This theorem is referenced by:  chvarv  1855  ru  2823  nalset  3928  tfisi  4356  tfr1onlemsucfn  6009  tfr1onlemsucaccv  6010  tfr1onlembxssdm  6012  tfr1onlembfn  6013  tfr1onlemres  6018  tfri1dALT  6020  tfrcllemsucfn  6022  tfrcllemsucaccv  6023  tfrcllembxssdm  6025  tfrcllembfn  6026  tfrcllemres  6031  findcard2  6445  findcard2s  6446  bj-nalset  10953