Axiom ax-4

Description: Axiom of Quantified Implication. Axiom C4 of Monk2 p. 105 and Theorem 19.20 of Margaris p. 90. It is restated as alim for labeling consistency. It should be used only by alim . (Contributed by NM, 21-May-2008) Use alim instead. (New usage is discouraged.)

	Ref	Expression
Assertion	ax-4	|- ( A. x ( ph -> ps ) -> ( A. x ph -> A. x ps ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	|- x
1		wph	|- ph
2		wps	|- ps
3	1 2	wi	|- ( ph -> ps )
4	3 0	wal	|- A. x ( ph -> ps )
5	1 0	wal	|- A. x ph
6	2 0	wal	|- A. x ps
7	5 6	wi	|- ( A. x ph -> A. x ps )
8	4 7	wi	|- ( A. x ( ph -> ps ) -> ( A. x ph -> A. x ps ) )