Theorem alim 1813

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

Assertion

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

Proof of Theorem alim

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

Syntax hints:   → wi 4  ∀wal 1540

This theorem was proved from axioms:  ax-4 1812

This theorem is referenced by:  alimi  1814  al2im  1817  sylgt  1825  19.38a  1843  stdpc5v  1942  axc4  2315  hbaltg  34779  bj-2alim  35488  bj-alexim  35504  bj-cbvalimt  35516  bj-eximALT  35518  bj-hbalt  35559  bj-nfdt0  35573  bj-nnf-alrim  35633  bj-nnflemaa  35640  bj-nnflemea  35643  stdpc5t  35705  al3im  42398  hbalg  43316  al2imVD  43623  hbalgVD  43666