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  2324  hbaltg  35921  bj-2alim  36726  bj-sylggt  36733  bj-alexim  36743  bj-cbvalimt  36755  bj-eximALT  36757  bj-hbalt  36798  bj-nfdt0  36812  bj-nnf-alrim  36872  bj-nnflemaa  36879  bj-nnflemea  36882  stdpc5t  36944  al3im  43804  hbalg  44712  al2imVD  45018  hbalgVD  45061