![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ralrimdva | Structured version Visualization version GIF version |
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 2-Feb-2008.) (Proof shortened by Wolf Lammen, 28-Dec-2019.) |
Ref | Expression |
---|---|
ralrimdva.1 | ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒)) |
Ref | Expression |
---|---|
ralrimdva | ⊢ (𝜑 → (𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralrimdva.1 | . . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒)) | |
2 | 1 | expimpd 457 | . . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) → 𝜒)) |
3 | 2 | expcomd 420 | . 2 ⊢ (𝜑 → (𝜓 → (𝑥 ∈ 𝐴 → 𝜒))) |
4 | 3 | ralrimdv 3153 | 1 ⊢ (𝜑 → (𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∈ wcel 2111 ∀wral 3106 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ral 3111 |
This theorem is referenced by: ralxfrd 5274 ralxfrd2 5278 isoselem 7073 resixpfo 8483 findcard 8741 ordtypelem2 8967 alephinit 9506 isfin2-2 9730 axpre-sup 10580 nnsub 11669 ublbneg 12321 xralrple 12586 supxrunb1 12700 expnlbnd2 13591 faclbnd4lem4 13652 hashbc 13807 cau3lem 14706 limsupbnd2 14832 climrlim2 14896 climshftlem 14923 subcn2 14943 isercoll 15016 climsup 15018 serf0 15029 iseralt 15033 incexclem 15183 sqrt2irr 15594 pclem 16165 prmpwdvds 16230 vdwlem10 16316 vdwlem13 16319 ramtlecl 16326 ramub 16339 ramcl 16355 iscatd 16936 clatleglb 17728 mndind 17984 grpinveu 18130 dfgrp3lem 18189 issubg4 18290 gexdvds 18701 sylow2alem2 18735 obselocv 20417 scmatscm 21118 tgcn 21857 tgcnp 21858 lmconst 21866 cncls2 21878 cncls 21879 cnntr 21880 lmss 21903 cnt0 21951 isnrm2 21963 isreg2 21982 cmpsublem 22004 cmpsub 22005 tgcmp 22006 islly2 22089 kgencn2 22162 txdis 22237 txlm 22253 kqt0lem 22341 isr0 22342 regr1lem2 22345 cmphaushmeo 22405 cfinufil 22533 ufilen 22535 flimopn 22580 fbflim2 22582 fclsnei 22624 fclsbas 22626 fclsrest 22629 flimfnfcls 22633 fclscmp 22635 ufilcmp 22637 isfcf 22639 fcfnei 22640 cnpfcf 22646 tsmsres 22749 tsmsxp 22760 blbas 23037 prdsbl 23098 metss 23115 metcnp3 23147 bndth 23563 lebnumii 23571 iscfil3 23877 iscmet3lem1 23895 equivcfil 23903 equivcau 23904 ellimc3 24482 lhop1 24617 dvfsumrlim 24634 ftc1lem6 24644 fta1g 24768 dgrco 24872 plydivex 24893 fta1 24904 vieta1 24908 ulmshftlem 24984 ulmcaulem 24989 mtest 24999 cxpcn3lem 25336 cxploglim 25563 ftalem3 25660 dchrisumlem3 26075 pntibnd 26177 ostth2lem2 26218 grpoinveu 28302 nmcvcn 28478 blocnilem 28587 ubthlem3 28655 htthlem 28700 spansni 29340 bra11 29891 lmxrge0 31305 mrsubff1 32874 msubff1 32916 fnemeet2 33828 fnejoin2 33830 fin2so 35044 lindsenlbs 35052 poimirlem29 35086 poimirlem30 35087 ftc1cnnc 35129 incsequz2 35187 geomcau 35197 caushft 35199 sstotbnd2 35212 isbnd2 35221 totbndbnd 35227 ismtybndlem 35244 heibor 35259 atlatle 36616 cvlcvr1 36635 ltrnid 37431 ltrneq2 37444 climinf 42248 ralbinrald 43678 snlindsntorlem 44879 |
Copyright terms: Public domain | W3C validator |