Theorem a4v 1267

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

Syntax hints:   -> wi 3   <-> wb 146  A.wal 951   = wceq 953

This theorem is referenced by:  chvarv 1322  ru 1928  sbcralt 1980  nalset 2702  dtruALT 2738  asymref2 3424  asymref2OLD 3426  setind 4620  karden 4698  prlem934a 5109  suppsr2 5195  islp2 7688  axgroth3 8718  grothinf 8720

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-17 968  ax-4 970  ax-5o 972  ax-9o 1119

This theorem depends on definitions:  df-bi 147

Copyright terms: Public domain