![]() |
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 630 | . . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) → 𝜒)) |
3 | 2 | expcomd 453 | . 2 ⊢ (𝜑 → (𝜓 → (𝑥 ∈ 𝐴 → 𝜒))) |
4 | 3 | ralrimdv 3106 | 1 ⊢ (𝜑 → (𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∈ wcel 2139 ∀wral 3050 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 ax-5 1988 |
This theorem depends on definitions: df-bi 197 df-an 385 df-ral 3055 |
This theorem is referenced by: ralxfrd 5028 ralxfrdOLD 5029 ralxfrd2 5033 isoselem 6755 resixpfo 8114 findcard 8366 ordtypelem2 8591 alephinit 9128 isfin2-2 9353 axpre-sup 10202 nnsub 11271 ublbneg 11986 xralrple 12249 supxrunb1 12362 expnlbnd2 13209 faclbnd4lem4 13297 hashbc 13449 cau3lem 14313 limsupbnd2 14433 climrlim2 14497 climshftlem 14524 subcn2 14544 isercoll 14617 climsup 14619 serf0 14630 iseralt 14634 incexclem 14787 sqrt2irr 15198 pclem 15765 prmpwdvds 15830 vdwlem10 15916 vdwlem13 15919 ramtlecl 15926 ramub 15939 ramcl 15955 iscatd 16555 clatleglb 17347 mrcmndind 17587 grpinveu 17677 dfgrp3lem 17734 issubg4 17834 gexdvds 18219 sylow2alem2 18253 obselocv 20294 scmatscm 20541 tgcn 21278 tgcnp 21279 lmconst 21287 cncls2 21299 cncls 21300 cnntr 21301 lmss 21324 cnt0 21372 isnrm2 21384 isreg2 21403 cmpsublem 21424 cmpsub 21425 tgcmp 21426 islly2 21509 kgencn2 21582 txdis 21657 txlm 21673 kqt0lem 21761 isr0 21762 regr1lem2 21765 cmphaushmeo 21825 cfinufil 21953 ufilen 21955 flimopn 22000 fbflim2 22002 fclsnei 22044 fclsbas 22046 fclsrest 22049 flimfnfcls 22053 fclscmp 22055 ufilcmp 22057 isfcf 22059 fcfnei 22060 cnpfcf 22066 tsmsres 22168 tsmsxp 22179 blbas 22456 prdsbl 22517 metss 22534 metcnp3 22566 bndth 22978 lebnumii 22986 iscfil3 23291 iscmet3lem1 23309 equivcfil 23317 equivcau 23318 ellimc3 23862 lhop1 23996 dvfsumrlim 24013 ftc1lem6 24023 fta1g 24146 dgrco 24250 plydivex 24271 fta1 24282 vieta1 24286 ulmshftlem 24362 ulmcaulem 24367 mtest 24377 cxpcn3lem 24708 cxploglim 24924 ftalem3 25021 dchrisumlem3 25400 pntibnd 25502 ostth2lem2 25543 grpoinveu 27703 nmcvcn 27880 blocnilem 27989 ubthlem3 28058 htthlem 28104 spansni 28746 bra11 29297 lmxrge0 30328 mrsubff1 31739 msubff1 31781 fnemeet2 32689 fnejoin2 32691 fin2so 33727 lindsenlbs 33735 poimirlem29 33769 poimirlem30 33770 ftc1cnnc 33815 incsequz2 33876 geomcau 33886 caushft 33888 sstotbnd2 33904 isbnd2 33913 totbndbnd 33919 ismtybndlem 33936 heibor 33951 atlatle 35128 cvlcvr1 35147 ltrnid 35942 ltrneq2 35955 climinf 40359 ralbinrald 41723 snlindsntorlem 42787 |
Copyright terms: Public domain | W3C validator |