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  2326  hbaltg  35999  bj-2alim  36810  bj-sylggt  36817  bj-alexim  36827  bj-cbvalimt  36839  bj-eximALT  36841  bj-hbalt  36882  bj-nfdt0  36896  bj-nnf-alrim  36956  bj-nnflemaa  36963  bj-nnflemea  36966  stdpc5t  37028  al3im  43888  hbalg  44796  al2imVD  45102  hbalgVD  45145