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  1973  axc4  2355  hbaltg  36784  bj-almp  37696  bj-sylggt  37697  bj-2alim  37707  bj-exim  37724  bj-alexim  37725  bj-nfdt0  37812  bj-nnf-alrim  37862  bj-nnflemaa  37903  bj-nnflemea  37906  stdpc5t  37954  al3im  44908  hbalg  45798  al2imVD  46104  hbalgVD  46147