Theorem alim 1843

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

Assertion

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

Proof of Theorem alim

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1568

This proof depends on axioms:  ax-4 1842

This theorem is used by:  alimi  1844  al2im  1847  sylgt  1855  19.38a  1873  stdpc5v  1971  axc4  2351  hbaltg  36387  bj-almp  37315  bj-sylggt  37316  bj-2alim  37326  bj-exim  37343  bj-alexim  37344  bj-nfdt0  37431  bj-nnf-alrim  37481  bj-nnflemaa  37522  bj-nnflemea  37525  stdpc5t  37573  al3im  44490  hbalg  45381  al2imVD  45687  hbalgVD  45730