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 1539

This theorem was proved from axioms:  ax-4 1810

This theorem is referenced by:  alimi  1812  al2im  1815  sylgt  1823  19.38a  1841  stdpc5v  1939  axc4  2322  hbaltg  35841  bj-2alim  36644  bj-sylggt  36651  bj-alexim  36661  bj-cbvalimt  36673  bj-eximALT  36675  bj-hbalt  36715  bj-nfdt0  36729  bj-nnf-alrim  36789  bj-nnflemaa  36796  bj-nnflemea  36799  stdpc5t  36861  al3im  43680  hbalg  44588  al2imVD  44894  hbalgVD  44937