Theorem a4imv 1203

Description: A version of a4im 1155 with a distinct variable requirement instead of a bound variable hypothesis.

Hypothesis

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

Assertion

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

Distinct variable group:   ps,x

Proof of Theorem a4imv

Step	Hyp	Ref	Expression
1		ax-17 968	. 2 |- (ps -> A.xps)
2		a4imv.1	. 2 |- (x = y -> (ph -> ps))
3	1, 2	a4im 1155	1 |- (A.xph -> ps)

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

This theorem is referenced by:  aev 1204  ax16i 1265  a4v 1267  reu3 1921

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

Copyright terms: Public domain