Theorem a4v 1310

Description: Specialization, using implicit substitition.

Hypothesis

Ref	Expression
a4v.1	|- (x = y -> (ph <-> ps))

Assertion

Ref	Expression
a4v	|- (A.xph -> ps)

Distinct variable group:   ps,x

Proof of Theorem a4v

Step	Hyp	Ref	Expression
1		a4v.1	. . 3 |- (x = y -> (ph <-> ps))
2	1	biimpd 151	. 2 |- (x = y -> (ph -> ps))
3	2	a4imv 1244	1 |- (A.xph -> ps)

Syntax hints:   -> wi 3   <-> wb 144  A.wal 990   = wceq 992

This theorem is referenced by:  chvarv 1365  ru 1984  sbcralt 2040  nalset 2786  el 2822  dtru 2831  asymref2 3532  setind 4794  karden 4872  prlem934a 5291  suppsr2 5377  islp2 7957  axgroth3 9051  grothinf 9053  trer 11409  ordtypelem5 11431  ordtypelem6 11432  alexsublem3 11498  limfilcf 11683  fcluscf 11724  inficl 11849

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 999  ax-17 1007  ax-4 1009  ax-5o 1011  ax-9o 1159

This theorem depends on definitions:  df-bi 145

Copyright terms: Public domain