Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > axc4i | Structured version Visualization version GIF version |
Description: Inference version of axc4 2115. (Contributed by NM, 3-Jan-1993.) |
Ref | Expression |
---|---|
axc4i.1 | ⊢ (∀𝑥𝜑 → 𝜓) |
Ref | Expression |
---|---|
axc4i | ⊢ (∀𝑥𝜑 → ∀𝑥𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfa1 2015 | . 2 ⊢ Ⅎ𝑥∀𝑥𝜑 | |
2 | axc4i.1 | . 2 ⊢ (∀𝑥𝜑 → 𝜓) | |
3 | 1, 2 | alrimi 2069 | 1 ⊢ (∀𝑥𝜑 → ∀𝑥𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1473 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-12 2034 |
This theorem depends on definitions: df-bi 196 df-or 384 df-ex 1696 df-nf 1701 |
This theorem is referenced by: hbae 2303 hbsb2 2347 hbsb2a 2349 hbsb2e 2351 reu6 3362 axunndlem1 9296 axacndlem3 9310 axacndlem5 9312 axacnd 9313 bj-nfs1t 31901 bj-hbs1 31946 bj-hbsb2av 31948 bj-hbaeb2 31993 wl-hbae1 32482 frege93 37270 pm11.57 37611 pm11.59 37613 axc5c4c711toc7 37627 axc11next 37629 hbalg 37792 ax6e2eq 37794 ax6e2eqVD 38165 |
Copyright terms: Public domain | W3C validator |