Theorem alim 1808

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

Assertion

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

Proof of Theorem alim

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

Syntax hints:   → wi 4  ∀wal 1535

This theorem was proved from axioms:  ax-4 1807

This theorem is referenced by:  alimi  1809  al2im  1812  sylgt  1820  19.38a  1838  stdpc5v  1937  axc4  2325  hbaltg  35771  bj-2alim  36576  bj-sylggt  36583  bj-alexim  36593  bj-cbvalimt  36605  bj-eximALT  36607  bj-hbalt  36647  bj-nfdt0  36661  bj-nnf-alrim  36721  bj-nnflemaa  36728  bj-nnflemea  36731  stdpc5t  36793  al3im  43609  hbalg  44526  al2imVD  44833  hbalgVD  44876