![]() |
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 1807. See alimdh 1814 and alimd 2210 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 1908 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) | |
2 | alimdv.1 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
3 | 1, 2 | alimdh 1814 | 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-gen 1792 ax-4 1806 ax-5 1908 |
This theorem is referenced by: 2alimdv 1916 ax12v2 2177 ax13lem1 2377 axc16i 2439 mo4 2564 ralimdv2 3161 mo2icl 3723 sstr2OLD 4003 reuss2 4332 ssuni 4937 disjss2 5118 disjss1 5121 disjiun 5136 disjss3 5147 alxfr 5413 axprlem1 5429 axprlem2 5430 axpr 5433 axprOLD 5437 frss 5653 ssrel 5795 ssrelOLD 5796 ssrel2 5798 ssrelrel 5809 iotavalOLD 6537 fvn0ssdmfun 7094 dff3 7120 dfwe2 7793 trom 7896 findcard3 9316 findcard3OLD 9317 dffi2 9461 indcardi 10079 zorn2lem4 10537 uzindi 14020 caubnd 15394 ramtlecl 17034 psgnunilem4 19530 nrhmzr 20554 dfconn2 23443 wilthlem3 27128 disjss1f 32592 ssrelf 32635 axsepg2 35075 axsepg2ALT 35076 ss2mcls 35553 mclsax 35554 wzel 35806 onsuct0 36424 bj-zfauscl 36907 wl-ax13lem1 37477 axc11next 44402 traxext 44938 iscnrm3lem2 48731 setrec1lem2 48919 |
Copyright terms: Public domain | W3C validator |