Theorem alim 1811

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

Assertion

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

Proof of Theorem alim

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

Syntax hints:   → wi 4  ∀wal 1535

This theorem was proved from axioms:  ax-4 1810

This theorem is referenced by:  alimi  1812  al2im  1815  sylgt  1822  19.38a  1840  stdpc5v  1939  axc4  2340  hbaltg  33054  bj-2alim  33946  bj-alexim  33962  bj-cbvalimt  33974  bj-eximALT  33976  bj-hbalt  34017  bj-nfdt0  34031  bj-nnf-alrim  34086  bj-nnflemaa  34093  bj-nnflemea  34096  stdpc5t  34152  al3im  39998  hbalg  40896  al2imVD  41203  hbalgVD  41246