| 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 453 | . . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) → 𝜒)) |
| 3 | 2 | expcomd 416 | . 2 ⊢ (𝜑 → (𝜓 → (𝑥 ∈ 𝐴 → 𝜒))) |
| 4 | 3 | ralrimdv 3152 | 1 ⊢ (𝜑 → (𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∈ wcel 2108 ∀wral 3061 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ral 3062 |
| This theorem is referenced by: ralxfrd 5408 ralxfrd2 5412 isoselem 7361 resixpfo 8976 findcard 9203 ordtypelem2 9559 alephinit 10135 isfin2-2 10359 axpre-sup 11209 nnsub 12310 ublbneg 12975 xralrple 13247 supxrunb1 13361 expnlbnd2 14273 faclbnd4lem4 14335 hashbc 14492 cau3lem 15393 limsupbnd2 15519 climrlim2 15583 climshftlem 15610 subcn2 15631 isercoll 15704 climsup 15706 serf0 15717 iseralt 15721 incexclem 15872 sqrt2irr 16285 pclem 16876 prmpwdvds 16942 vdwlem10 17028 vdwlem13 17031 ramtlecl 17038 ramub 17051 ramcl 17067 iscatd 17716 clatleglb 18563 mndind 18841 grpinveu 18992 dfgrp3lem 19056 issubg4 19163 gexdvds 19602 sylow2alem2 19636 obselocv 21748 scmatscm 22519 tgcn 23260 tgcnp 23261 lmconst 23269 cncls2 23281 cncls 23282 cnntr 23283 lmss 23306 cnt0 23354 isnrm2 23366 isreg2 23385 cmpsublem 23407 cmpsub 23408 tgcmp 23409 islly2 23492 kgencn2 23565 txdis 23640 txlm 23656 kqt0lem 23744 isr0 23745 regr1lem2 23748 cmphaushmeo 23808 cfinufil 23936 ufilen 23938 flimopn 23983 fbflim2 23985 fclsnei 24027 fclsbas 24029 fclsrest 24032 flimfnfcls 24036 fclscmp 24038 ufilcmp 24040 isfcf 24042 fcfnei 24043 cnpfcf 24049 tsmsres 24152 tsmsxp 24163 blbas 24440 prdsbl 24504 metss 24521 metcnp3 24553 bndth 24990 lebnumii 24998 iscfil3 25307 iscmet3lem1 25325 equivcfil 25333 equivcau 25334 ellimc3 25914 lhop1 26053 dvfsumrlim 26072 ftc1lem6 26082 fta1g 26209 dgrco 26315 plydivex 26339 fta1 26350 vieta1 26354 ulmshftlem 26432 ulmcaulem 26437 mtest 26447 cxpcn3lem 26790 cxploglim 27021 ftalem3 27118 dchrisumlem3 27535 pntibnd 27637 ostth2lem2 27678 n0subs 28360 grpoinveu 30538 nmcvcn 30714 blocnilem 30823 ubthlem3 30891 htthlem 30936 spansni 31576 bra11 32127 lmxrge0 33951 mrsubff1 35519 msubff1 35561 fnemeet2 36368 fnejoin2 36370 fin2so 37614 lindsenlbs 37622 poimirlem29 37656 poimirlem30 37657 ftc1cnnc 37699 incsequz2 37756 geomcau 37766 caushft 37768 sstotbnd2 37781 isbnd2 37790 totbndbnd 37796 ismtybndlem 37813 heibor 37828 atlatle 39321 cvlcvr1 39340 ltrnid 40137 ltrneq2 40150 nadd1suc 43405 climinf 45621 ralbinrald 47134 snlindsntorlem 48387 |
| Copyright terms: Public domain | W3C validator |