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 1738. (Contributed by NM, 3-Apr-1994.) |
Ref | Expression |
---|---|
alimdv.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
Ref | Expression |
---|---|
alimdv | ⊢ (𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-5 1839 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) | |
2 | alimdv.1 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
3 | 1, 2 | alimdh 1745 | 1 ⊢ (𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1481 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-gen 1722 ax-4 1737 ax-5 1839 |
This theorem is referenced by: 2alimdv 1847 ax12v2 2049 ax12vOLD 2050 ax12vOLDOLD 2051 ax13lem1 2248 axc16i 2322 ralimdv2 2961 mo2icl 3385 sstr2 3610 reuss2 3907 ssuni 4459 ssuniOLD 4460 disjss2 4623 disjss1 4626 disjiun 4640 disjss3 4652 alxfr 4878 frss 5081 ssrel 5207 ssrelOLD 5208 ssrel2 5210 ssrelrel 5220 iotaval 5862 fvn0ssdmfun 6350 dff3 6372 dfwe2 6981 ordom 7074 findcard3 8203 dffi2 8329 indcardi 8864 zorn2lem4 9321 uzindi 12781 caubnd 14098 ramtlecl 15704 psgnunilem4 17917 dfconn2 21222 wilthlem3 24796 disjss1f 29386 ssrelf 29425 ss2mcls 31465 mclsax 31466 wzel 31771 wzelOLD 31772 onsuct0 32440 bj-ssbim 32621 wl-ax13lem1 33287 wl-ax8clv2 33381 axc11next 38607 nrhmzr 41873 setrec1lem2 42435 |
Copyright terms: Public domain | W3C validator |