Theorem a4v 1272

Description: Specialization with implicit substitution.

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

Syntax hints:   -> wi 3   <-> wb 146  A.wal 954   = wceq 956

This theorem is referenced by:  chvarv 1327  ru 1938  sbcralt 1990  nalset 2712  dtruALT 2748  asymref2 3440  setind 4648  karden 4726  prlem934a 5137  suppsr2 5223  islp2 7747  axgroth3 8779  grothinf 8781

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-17 971  ax-4 973  ax-5o 975  ax-9o 1123

This theorem depends on definitions:  df-bi 147

Copyright terms: Public domain