Theorem spv 1848

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 1799	1 |- ( A. x ph -> ps )

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

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 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522

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

This theorem is referenced by:  spvv  1895  cbvalvw  1907  chvarv  1925  ru  2950  nalset  4112  tfisi  4564  tfr1onlemsucfn  6308  tfr1onlemsucaccv  6309  tfr1onlembxssdm  6311  tfr1onlembfn  6312  tfr1onlemres  6317  tfri1dALT  6319  tfrcllemsucfn  6321  tfrcllemsucaccv  6322  tfrcllembxssdm  6324  tfrcllembfn  6325  tfrcllemres  6330  findcard2  6855  findcard2s  6856  bj-nalset  13777