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  2356  hbaltg  36336  bj-almp  37263  bj-sylggt  37264  bj-2alim  37274  bj-exim  37291  bj-alexim  37292  bj-nfdt0  37379  bj-nnf-alrim  37429  bj-nnflemaa  37470  bj-nnflemea  37473  stdpc5t  37521  al3im  44433  hbalg  45324  al2imVD  45630  hbalgVD  45673