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 1729. (Contributed by NM, 3-Apr-1994.) |
Ref | Expression |
---|---|
alimdv.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
Ref | Expression |
---|---|
alimdv | ⊢ (𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-5 1827 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) | |
2 | alimdv.1 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
3 | 1, 2 | alimdh 1735 | 1 ⊢ (𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1473 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-gen 1713 ax-4 1728 ax-5 1827 |
This theorem is referenced by: 2alimdv 1834 ax12v2 2036 ax12vOLD 2037 ax12vOLDOLD 2038 ax13lem1 2236 axc16i 2310 ralimdv2 2944 mo2icl 3352 sstr2 3575 reuss2 3866 ssuni 4395 ssuniOLD 4396 disjss2 4556 disjss1 4559 disjiun 4573 disjss3 4582 alxfr 4804 frss 5005 ssrel 5130 ssrelOLD 5131 ssrel2 5133 ssrelrel 5143 iotaval 5779 fvn0ssdmfun 6258 dff3 6280 dfwe2 6873 ordom 6966 findcard3 8088 dffi2 8212 indcardi 8747 zorn2lem4 9204 uzindi 12643 caubnd 13946 ramtlecl 15542 psgnunilem4 17740 dfcon2 21032 wilthlem3 24596 nbcusgra 25992 disjss1f 28768 ssrelf 28805 ss2mcls 30719 mclsax 30720 wzel 31015 wzelOLD 31016 onsuct0 31610 bj-ssbim 31810 wl-ax13lem1 32466 axc11next 37629 nrhmzr 41663 setrec1lem2 42234 |
Copyright terms: Public domain | W3C validator |