Theorem alim 1814

Description: Restatement of Axiom ax-4 1813, for labeling consistency. It should be the only theorem using ax-4 1813. (Contributed by NM, 10-Jan-1993.)

Assertion

Ref	Expression
alim	⊢ (∀𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓))

Proof of Theorem alim

Step	Hyp	Ref	Expression
1		ax-4 1813	1 ⊢ (∀𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓))

Syntax hints:   → wi 4  ∀wal 1537

This theorem was proved from axioms:  ax-4 1813

This theorem is referenced by:  alimi  1815  al2im  1818  sylgt  1825  19.38a  1843  stdpc5v  1942  axc4  2319  hbaltg  33689  bj-2alim  34719  bj-alexim  34735  bj-cbvalimt  34747  bj-eximALT  34749  bj-hbalt  34790  bj-nfdt0  34804  bj-nnf-alrim  34864  bj-nnflemaa  34871  bj-nnflemea  34874  stdpc5t  34937  al3im  41144  hbalg  42064  al2imVD  42371  hbalgVD  42414