![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > alimdv | Structured version Visualization version GIF version |
Description: Deduction form of Theorem 19.20 of [Margaris] p. 90, see alim 1813. See alimdh 1820 and alimd 2206 for versions without a distinct variable condition. (Contributed by NM, 3-Apr-1994.) |
Ref | Expression |
---|---|
alimdv.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
Ref | Expression |
---|---|
alimdv | ⊢ (𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-5 1914 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) | |
2 | alimdv.1 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
3 | 1, 2 | alimdh 1820 | 1 ⊢ (𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1540 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-gen 1798 ax-4 1812 ax-5 1914 |
This theorem is referenced by: 2alimdv 1922 ax12v2 2174 ax13lem1 2373 axc16i 2435 mo4 2561 ralimdv2 3157 mo2icl 3676 sstr2 3955 reuss2 4279 ssuni 4897 disjss2 5077 disjss1 5080 disjiun 5096 disjss3 5108 alxfr 5366 axprlem1 5382 axprlem2 5383 axpr 5387 frss 5604 ssrel 5742 ssrelOLD 5743 ssrel2 5745 ssrelrel 5756 iotavalOLD 6474 fvn0ssdmfun 7029 dff3 7054 dfwe2 7712 trom 7815 findcard3 9235 findcard3OLD 9236 dffi2 9367 indcardi 9985 zorn2lem4 10443 uzindi 13896 caubnd 15252 ramtlecl 16880 psgnunilem4 19287 dfconn2 22793 wilthlem3 26442 disjss1f 31543 ssrelf 31587 ss2mcls 34226 mclsax 34227 wzel 34462 onsuct0 34966 bj-zfauscl 35444 wl-ax13lem1 36015 axc11next 42778 nrhmzr 46261 iscnrm3lem2 47057 setrec1lem2 47223 |
Copyright terms: Public domain | W3C validator |