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 454 | . . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) → 𝜒)) |
3 | 2 | expcomd 417 | . 2 ⊢ (𝜑 → (𝜓 → (𝑥 ∈ 𝐴 → 𝜒))) |
4 | 3 | ralrimdv 3114 | 1 ⊢ (𝜑 → (𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∈ wcel 2110 ∀wral 3066 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ral 3071 |
This theorem is referenced by: ralxfrd 5335 ralxfrd2 5339 isoselem 7206 resixpfo 8705 findcard 8926 ordtypelem2 9254 alephinit 9850 isfin2-2 10074 axpre-sup 10924 nnsub 12015 ublbneg 12670 xralrple 12936 supxrunb1 13050 expnlbnd2 13945 faclbnd4lem4 14006 hashbc 14161 cau3lem 15062 limsupbnd2 15188 climrlim2 15252 climshftlem 15279 subcn2 15300 isercoll 15375 climsup 15377 serf0 15388 iseralt 15392 incexclem 15544 sqrt2irr 15954 pclem 16535 prmpwdvds 16601 vdwlem10 16687 vdwlem13 16690 ramtlecl 16697 ramub 16710 ramcl 16726 iscatd 17378 clatleglb 18232 mndind 18462 grpinveu 18610 dfgrp3lem 18669 issubg4 18770 gexdvds 19185 sylow2alem2 19219 obselocv 20931 scmatscm 21658 tgcn 22399 tgcnp 22400 lmconst 22408 cncls2 22420 cncls 22421 cnntr 22422 lmss 22445 cnt0 22493 isnrm2 22505 isreg2 22524 cmpsublem 22546 cmpsub 22547 tgcmp 22548 islly2 22631 kgencn2 22704 txdis 22779 txlm 22795 kqt0lem 22883 isr0 22884 regr1lem2 22887 cmphaushmeo 22947 cfinufil 23075 ufilen 23077 flimopn 23122 fbflim2 23124 fclsnei 23166 fclsbas 23168 fclsrest 23171 flimfnfcls 23175 fclscmp 23177 ufilcmp 23179 isfcf 23181 fcfnei 23182 cnpfcf 23188 tsmsres 23291 tsmsxp 23302 blbas 23579 prdsbl 23643 metss 23660 metcnp3 23692 bndth 24117 lebnumii 24125 iscfil3 24433 iscmet3lem1 24451 equivcfil 24459 equivcau 24460 ellimc3 25039 lhop1 25174 dvfsumrlim 25191 ftc1lem6 25201 fta1g 25328 dgrco 25432 plydivex 25453 fta1 25464 vieta1 25468 ulmshftlem 25544 ulmcaulem 25549 mtest 25559 cxpcn3lem 25896 cxploglim 26123 ftalem3 26220 dchrisumlem3 26635 pntibnd 26737 ostth2lem2 26778 grpoinveu 28875 nmcvcn 29051 blocnilem 29160 ubthlem3 29228 htthlem 29273 spansni 29913 bra11 30464 lmxrge0 31896 mrsubff1 33470 msubff1 33512 fnemeet2 34550 fnejoin2 34552 fin2so 35758 lindsenlbs 35766 poimirlem29 35800 poimirlem30 35801 ftc1cnnc 35843 incsequz2 35901 geomcau 35911 caushft 35913 sstotbnd2 35926 isbnd2 35935 totbndbnd 35941 ismtybndlem 35958 heibor 35973 atlatle 37328 cvlcvr1 37347 ltrnid 38143 ltrneq2 38156 climinf 43116 ralbinrald 44580 snlindsntorlem 45778 |
Copyright terms: Public domain | W3C validator |