| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > ralimdv | Structured version Visualization version GIF version | ||
| Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90 (alim 1810). (Contributed by NM, 8-Oct-2003.) |
| Ref | Expression |
|---|---|
| ralimdv.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
| Ref | Expression |
|---|---|
| ralimdv | ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ralimdv.1 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
| 2 | 1 | adantr 480 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒)) |
| 3 | 2 | ralimdva 3146 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∈ wcel 2109 ∀wral 3045 |
| 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 3046 |
| This theorem is referenced by: r19.21v 3159 ralimdvv 3187 ss2ralv 4020 poss 5551 sess1 5606 sess2 5607 riinint 5938 iinpreima 7044 dffo4 7078 dffo5 7079 isoini2 7317 tfindsg 7840 el2mpocsbcl 8067 xpord3inddlem 8136 iiner 8765 xpf1o 9109 dffi3 9389 brwdom3 9542 xpwdomg 9545 ttrclss 9680 bndrank 9801 cfub 10209 cff1 10218 cfflb 10219 cfslb2n 10228 cofsmo 10229 cfcoflem 10232 pwcfsdom 10543 fpwwe2lem12 10602 inawinalem 10649 grupr 10757 fsequb 13947 cau3lem 15328 caubnd2 15331 caubnd 15332 rlim2lt 15470 rlim3 15471 climshftlem 15547 climcau 15644 caucvgb 15653 serf0 15654 modfsummods 15766 cvgcmp 15789 mreriincl 17566 acsfn1c 17630 islss4 20875 riinopn 22802 fiinbas 22846 baspartn 22848 isclo2 22982 lmcls 23196 lmcnp 23198 isnrm3 23253 1stcelcls 23355 llyss 23373 nllyss 23374 ptpjpre1 23465 txlly 23530 txnlly 23531 tx1stc 23544 xkococnlem 23553 fbunfip 23763 filssufilg 23805 cnpflf2 23894 fcfnei 23929 isucn2 24173 rescncf 24797 lebnum 24870 cfilss 25177 fgcfil 25178 iscau4 25186 cmetcaulem 25195 caussi 25204 ovolunlem1 25405 ulmclm 26303 ulmcaulem 26310 ulmcau 26311 ulmss 26313 rlimcnp 26882 cxploglim 26895 2sqreunnlem2 27373 pntlemp 27528 nosupno 27622 nosupres 27626 noinfno 27637 noinfres 27641 sssslt2 27715 madebdayim 27806 madebdaylemold 27816 axcontlem4 28901 ewlkle 29540 uspgr2wlkeq 29581 umgrwlknloop 29584 wlkiswwlksupgr2 29814 3cyclfrgrrn2 30223 nmlnoubi 30732 lnon0 30734 disjpreima 32520 resspos 32899 resstos 32900 submarchi 33147 prmidl2 33419 crefss 33846 iccllysconn 35244 cvmlift2lem1 35296 dmopab3rexdif 35399 ss2mcls 35562 mclsax 35563 isinf2 37400 poimirlem25 37646 poimirlem27 37648 upixp 37730 caushft 37762 sstotbnd3 37777 totbndss 37778 unichnidl 38032 ispridl2 38039 elrfirn2 42691 mzpsubst 42743 eluzrabdioph 42801 neik0pk1imk0 44043 mnuop3d 44267 ismnushort 44297 pwclaxpow 44981 limsupub 45709 limsupre3lem 45737 climuzlem 45748 xlimbr 45832 fourierdlem103 46214 fourierdlem104 46215 qndenserrnbllem 46299 2reuimp 47120 ralralimp 47283 |
| Copyright terms: Public domain | W3C validator |