| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > alim | Structured version Visualization version GIF version | ||
| Description: Restatement of Axiom ax-4 1809, for labeling consistency. It should be the only theorem using ax-4 1809. (Contributed by NM, 10-Jan-1993.) |
| Ref | Expression |
|---|---|
| alim | ⊢ (∀𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-4 1809 | 1 ⊢ (∀𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∀wal 1538 |
| This theorem was proved from axioms: ax-4 1809 |
| This theorem is referenced by: alimi 1811 al2im 1814 sylgt 1822 19.38a 1840 stdpc5v 1938 axc4 2321 hbaltg 35808 bj-2alim 36611 bj-sylggt 36618 bj-alexim 36628 bj-cbvalimt 36640 bj-eximALT 36642 bj-hbalt 36682 bj-nfdt0 36696 bj-nnf-alrim 36756 bj-nnflemaa 36763 bj-nnflemea 36766 stdpc5t 36828 al3im 43660 hbalg 44575 al2imVD 44882 hbalgVD 44925 |
| Copyright terms: Public domain | W3C validator |