![]() |
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 1773. (Contributed by NM, 3-Apr-1994.) |
Ref | Expression |
---|---|
alimdv.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
Ref | Expression |
---|---|
alimdv | ⊢ (𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-5 1869 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) | |
2 | alimdv.1 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
3 | 1, 2 | alimdh 1780 | 1 ⊢ (𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1505 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-gen 1758 ax-4 1772 ax-5 1869 |
This theorem is referenced by: 2alimdv 1877 ax12v2 2108 sbequivvOLD 2255 ax13lem1 2303 axc16i 2372 ralimdv2 3120 mo2icl 3613 sstr2 3859 reuss2 4164 ssuni 4728 disjss2 4894 disjss1 4897 disjiun 4911 disjss3 4922 alxfr 5155 axprlem1 5174 axprlem2 5175 axpr 5179 frss 5368 ssrel 5501 ssrel2 5503 ssrelrel 5513 iotaval 6157 fvn0ssdmfun 6661 dff3 6683 dfwe2 7306 ordom 7399 findcard3 8550 dffi2 8676 indcardi 9255 zorn2lem4 9713 uzindi 13159 caubnd 14573 ramtlecl 16186 psgnunilem4 18381 dfconn2 21725 wilthlem3 25343 disjss1f 30083 ssrelf 30124 ss2mcls 32335 mclsax 32336 wzel 32632 onsuct0 33309 bj-zfauscl 33738 wl-ax13lem1 34187 axc11next 40155 nrhmzr 43508 setrec1lem2 44158 |
Copyright terms: Public domain | W3C validator |