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 627 | . . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) → 𝜒)) |
3 | 2 | expcomd 453 | . 2 ⊢ (𝜑 → (𝜓 → (𝑥 ∈ 𝐴 → 𝜒))) |
4 | 3 | ralrimdv 2951 | 1 ⊢ (𝜑 → (𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∈ wcel 1977 ∀wral 2896 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 |
This theorem depends on definitions: df-bi 196 df-an 385 df-ral 2901 |
This theorem is referenced by: ralxfrd 4805 ralxfrdOLD 4806 ralxfrd2 4810 isoselem 6491 resixpfo 7832 findcard 8084 ordtypelem2 8307 alephinit 8801 isfin2-2 9024 axpre-sup 9869 nnsub 10936 ublbneg 11649 xralrple 11910 supxrunb1 12021 expnlbnd2 12857 faclbnd4lem4 12945 hashbc 13094 cau3lem 13942 limsupbnd2 14062 climrlim2 14126 climshftlem 14153 subcn2 14173 isercoll 14246 climsup 14248 serf0 14259 iseralt 14263 incexclem 14407 sqrt2irr 14817 pclem 15381 prmpwdvds 15446 vdwlem10 15532 vdwlem13 15535 ramtlecl 15542 ramub 15555 ramcl 15571 iscatd 16157 clatleglb 16949 mrcmndind 17189 grpinveu 17279 dfgrp3lem 17336 issubg4 17436 gexdvds 17822 sylow2alem2 17856 obselocv 19891 scmatscm 20138 tgcn 20866 tgcnp 20867 lmconst 20875 cncls2 20887 cncls 20888 cnntr 20889 lmss 20912 cnt0 20960 isnrm2 20972 isreg2 20991 cmpsublem 21012 cmpsub 21013 tgcmp 21014 islly2 21097 kgencn2 21170 txdis 21245 txlm 21261 kqt0lem 21349 isr0 21350 regr1lem2 21353 cmphaushmeo 21413 cfinufil 21542 ufilen 21544 flimopn 21589 fbflim2 21591 fclsnei 21633 fclsbas 21635 fclsrest 21638 flimfnfcls 21642 fclscmp 21644 ufilcmp 21646 isfcf 21648 fcfnei 21649 cnpfcf 21655 tsmsres 21757 tsmsxp 21768 blbas 22045 prdsbl 22106 metss 22123 metcnp3 22155 bndth 22565 lebnumii 22573 iscfil3 22879 iscmet3lem1 22897 equivcfil 22905 equivcau 22906 ellimc3 23449 lhop1 23581 dvfsumrlim 23598 ftc1lem6 23608 fta1g 23731 dgrco 23835 plydivex 23856 fta1 23867 vieta1 23871 ulmshftlem 23947 ulmcaulem 23952 mtest 23962 cxpcn3lem 24288 cxploglim 24504 ftalem3 24601 dchrisumlem3 24980 pntibnd 25082 ostth2lem2 25123 grpoinveu 26757 nmcvcn 26934 blocnilem 27043 ubthlem3 27112 htthlem 27158 spansni 27800 bra11 28351 lmxrge0 29326 mrsubff1 30665 msubff1 30707 fnemeet2 31532 fnejoin2 31534 fin2so 32566 lindsenlbs 32574 poimirlem29 32608 poimirlem30 32609 ftc1cnnc 32654 incsequz2 32715 geomcau 32725 caushft 32727 sstotbnd2 32743 isbnd2 32752 totbndbnd 32758 ismtybndlem 32775 heibor 32790 atlatle 33625 cvlcvr1 33644 ltrnid 34439 ltrneq2 34452 climinf 38673 ralbinrald 39848 snlindsntorlem 42053 |
Copyright terms: Public domain | W3C validator |