Theorem alim 1738

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

Assertion

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

Proof of Theorem alim

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

Syntax hints:   → wi 4  ∀wal 1481

This theorem was proved from axioms:  ax-4 1737

This theorem is referenced by:  alimi  1739  al2im  1742  sylgt  1749  19.38a  1767  stdpc5v  1867  spfwOLD  1966  19.21tOLDOLD  2074  axc4  2130  19.21t-1OLD  2212  eunex  4859  hbaltg  31713  bj-2alim  32594  bj-alexim  32605  bj-hbalt  32671  bj-nfdt0  32685  bj-eunex  32799  stdpc5t  32814  al3im  37938  hbalg  38771  al2imVD  39098  hbalgVD  39141