Axiom ax-c4

Description: Axiom of Quantified Implication. This axiom moves a universal quantifier from outside to inside an implication, quantifying ps . Notice that x must not be a free variable in the antecedent of the quantified implication, and we express this by binding ph to "protect" the axiom from a ph containing a free x . Axiom scheme C4' in Megill p. 448 (p. 16 of the preprint). It is a special case of Lemma 5 of Monk2 p. 108 and Axiom 5 of Mendelson p. 69.

This axiom is obsolete and should no longer be used. It is proved above as theorem axc4 . (Contributed by NM, 3-Jan-1993) (New usage is discouraged.)

	Ref	Expression
Assertion	ax-c4	$$⊢\forall x\left(\forall x\phi \to \psi \right)\to \left(\forall x\phi \to \forall x\psi \right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	$$setvarx$$
1		wph	$$wff\phi$$
2	1 0	wal	$$wff\forall x\phi$$
3		wps	$$wff\psi$$
4	2 3	wi	$$wff\left(\forall x\phi \to \psi \right)$$
5	4 0	wal	$$wff\forall x\left(\forall x\phi \to \psi \right)$$
6	3 0	wal	$$wff\forall x\psi$$
7	2 6	wi	$$wff\left(\forall x\phi \to \forall x\psi \right)$$
8	5 7	wi	$$wff\left(\forall x\left(\forall x\phi \to \psi \right)\to \left(\forall x\phi \to \forall x\psi \right)\right)$$