Theorem a4v 1314

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 160	. 2 |- (x = y -> (ph -> ps))
3	2	a4imv 1249	1 |- (A.xph -> ps)

Syntax hints:   -> wi 3   <-> wb 153  A.wal 995   = wceq 997

This theorem is referenced by:  chvarv 1369  ru 1985  sbcralt 2040  nalset 2767  dtruALT 2804  asymref2 3497  setind 4710  karden 4788  prlem934a 5202  suppsr2 5288  islp2 7832  axgroth3 8862  grothinf 8864

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1004  ax-17 1012  ax-4 1014  ax-5o 1016  ax-9o 1164

This theorem depends on definitions:  df-bi 154

Copyright terms: Public domain