Theorem pm11.59

Description: Theorem *11.59 in WhiteheadRussell p. 165. (Contributed by Andrew Salmon, 25-May-2011)

	Ref	Expression
Assertion	pm11.59	|- ( A. x ( ph -> ps ) -> A. y A. x ( ( ph /\ [ y / x ] ph ) -> ( ps /\ [ y / x ] ps ) ) )

Proof

Step	Hyp	Ref	Expression
1		nfv	|- F/ y ( ph -> ps )
2	1	nfal	|- F/ y A. x ( ph -> ps )
3		sp	|- ( A. x ( ph -> ps ) -> ( ph -> ps ) )
4		spsbim	|- ( A. x ( ph -> ps ) -> ( [ y / x ] ph -> [ y / x ] ps ) )
5	3 4	anim12d	|- ( A. x ( ph -> ps ) -> ( ( ph /\ [ y / x ] ph ) -> ( ps /\ [ y / x ] ps ) ) )
6	5	axc4i	|- ( A. x ( ph -> ps ) -> A. x ( ( ph /\ [ y / x ] ph ) -> ( ps /\ [ y / x ] ps ) ) )
7	2 6	alrimi	|- ( A. x ( ph -> ps ) -> A. y A. x ( ( ph /\ [ y / x ] ph ) -> ( ps /\ [ y / x ] ps ) ) )