Theorem a4v 1274

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 1209	1 |- (A.xph -> ps)

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

This theorem is referenced by:  chvarv 1329  ru 1941  sbcralt 1994  nalset 2718  dtruALT 2755  asymref2 3447  setind 4665  karden 4743  prlem934a 5156  suppsr2 5242  islp2 7751  axgroth3 8781  grothinf 8783

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 965  ax-17 973  ax-4 975  ax-5o 977  ax-9o 1125

This theorem depends on definitions:  df-bi 147

Copyright terms: Public domain