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 1802. See alimdh 1809 and alimd 2203 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 1902 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) | |
2 | alimdv.1 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
3 | 1, 2 | alimdh 1809 | 1 ⊢ (𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1526 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-gen 1787 ax-4 1801 ax-5 1902 |
This theorem is referenced by: 2alimdv 1910 ax12v2 2169 sbequivvOLD 2326 ax13lem1 2385 axc16i 2453 mo4 2646 ralimdv2 3176 mo2icl 3704 sstr2 3973 reuss2 4282 ssuni 4854 disjss2 5026 disjss1 5029 disjiun 5045 disjss3 5057 alxfr 5299 axprlem1 5315 axprlem2 5316 axpr 5320 frss 5516 ssrel 5651 ssrel2 5653 ssrelrel 5663 iotaval 6323 fvn0ssdmfun 6835 dff3 6859 dfwe2 7484 ordom 7577 findcard3 8750 dffi2 8876 indcardi 9456 zorn2lem4 9910 uzindi 13340 caubnd 14708 ramtlecl 16326 psgnunilem4 18556 dfconn2 21957 wilthlem3 25575 disjss1f 30251 ssrelf 30295 ss2mcls 32713 mclsax 32714 wzel 33009 onsuct0 33687 bj-zfauscl 34141 wl-ax13lem1 34629 axc11next 40618 nrhmzr 44042 setrec1lem2 44689 |
Copyright terms: Public domain | W3C validator |