![]() |
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 1804. See alimdh 1811 and alimd 2197 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 1905 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) | |
2 | alimdv.1 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
3 | 1, 2 | alimdh 1811 | 1 ⊢ (𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1531 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-gen 1789 ax-4 1803 ax-5 1905 |
This theorem is referenced by: 2alimdv 1913 ax12v2 2165 ax13lem1 2365 axc16i 2427 mo4 2552 ralimdv2 3155 mo2icl 3703 sstr2 3982 reuss2 4308 ssuni 4927 disjss2 5107 disjss1 5110 disjiun 5126 disjss3 5138 alxfr 5396 axprlem1 5412 axprlem2 5413 axpr 5417 frss 5634 ssrel 5773 ssrelOLD 5774 ssrel2 5776 ssrelrel 5787 iotavalOLD 6508 fvn0ssdmfun 7067 dff3 7092 dfwe2 7755 trom 7858 findcard3 9282 findcard3OLD 9283 dffi2 9415 indcardi 10033 zorn2lem4 10491 uzindi 13945 caubnd 15303 ramtlecl 16934 psgnunilem4 19409 nrhmzr 20429 dfconn2 23247 wilthlem3 26921 disjss1f 32275 ssrelf 32316 ss2mcls 35050 mclsax 35051 wzel 35292 onsuct0 35817 bj-zfauscl 36295 wl-ax13lem1 36866 axc11next 43679 iscnrm3lem2 47779 setrec1lem2 47945 |
Copyright terms: Public domain | W3C validator |