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  2352  hbaltg  36569  bj-almp  37481  bj-sylggt  37482  bj-2alim  37492  bj-exim  37509  bj-alexim  37510  bj-nfdt0  37597  bj-nnf-alrim  37647  bj-nnflemaa  37688  bj-nnflemea  37691  stdpc5t  37739  al3im  44646  hbalg  45537  al2imVD  45843  hbalgVD  45886