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 2340. (Contributed by NM, 3-Jan-1993.) |
Ref | Expression |
---|---|
axc4i.1 | ⊢ (∀𝑥𝜑 → 𝜓) |
Ref | Expression |
---|---|
axc4i | ⊢ (∀𝑥𝜑 → ∀𝑥𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfa1 2155 | . 2 ⊢ Ⅎ𝑥∀𝑥𝜑 | |
2 | axc4i.1 | . 2 ⊢ (∀𝑥𝜑 → 𝜓) | |
3 | 1, 2 | alrimi 2213 | 1 ⊢ (∀𝑥𝜑 → ∀𝑥𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1535 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-10 2145 ax-12 2177 |
This theorem depends on definitions: df-bi 209 df-or 844 df-ex 1781 df-nf 1785 |
This theorem is referenced by: hbae 2453 hbsb2 2521 hbsb2a 2523 hbsb2e 2525 hbsb2ALT 2599 nfabdw 3002 reu6 3719 axunndlem1 10019 axacndlem3 10033 axacndlem5 10035 axacnd 10036 bj-nfs1t 34114 bj-hbs1 34136 bj-hbsb2av 34138 bj-hbaeb2 34143 wl-hbae1 34761 frege93 40309 spALT 40561 pm11.57 40728 pm11.59 40730 axc5c4c711toc7 40743 axc11next 40745 hbalg 40896 ax6e2eq 40898 ax6e2eqVD 41248 |
Copyright terms: Public domain | W3C validator |