Theorem alim 1805

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

Assertion

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

Proof of Theorem alim

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

Syntax hints:   → wi 4  ∀wal 1532

This theorem was proved from axioms:  ax-4 1804

This theorem is referenced by:  alimi  1806  al2im  1809  sylgt  1817  19.38a  1835  stdpc5v  1934  axc4  2309  hbaltg  35393  bj-2alim  36077  bj-alexim  36093  bj-cbvalimt  36105  bj-eximALT  36107  bj-hbalt  36148  bj-nfdt0  36162  bj-nnf-alrim  36222  bj-nnflemaa  36229  bj-nnflemea  36232  stdpc5t  36294  al3im  43049  hbalg  43966  al2imVD  44273  hbalgVD  44316