Theorem a4imv 1249

Description: A version of a4im 1201 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 1012	. 2 |- (ps -> A.xps)
2		a4imv.1	. 2 |- (x = y -> (ph -> ps))
3	1, 2	a4im 1201	1 |- (A.xph -> ps)

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

This theorem is referenced by:  aev 1250  ax16i 1312  a4v 1314  reu3 1978

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

Copyright terms: Public domain