![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ralimdv | Structured version Visualization version Unicode version |
Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90 (alim 1691). (Contributed by NM, 8-Oct-2003.) |
Ref | Expression |
---|---|
ralimdv.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
ralimdv |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralimdv.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | adantr 472 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | ralimdva 2805 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 |
This theorem depends on definitions: df-bi 190 df-an 378 df-ral 2761 |
This theorem is referenced by: poss 4762 sess1 4807 sess2 4808 riinint 5097 iinpreima 6025 dffo4 6053 dffo5 6054 isoini2 6248 tfindsg 6706 iiner 7453 xpf1o 7752 dffi3 7963 brwdom3 8115 xpwdomg 8118 bndrank 8330 cfub 8697 cff1 8706 cfflb 8707 cfslb2n 8716 cofsmo 8717 cfcoflem 8720 pwcfsdom 9026 fpwwe2lem13 9085 inawinalem 9132 grupr 9240 fsequb 12226 cau3lem 13494 caubnd2 13497 caubnd 13498 rlim2lt 13638 rlim3 13639 climshftlem 13715 isercolllem1 13805 climcau 13811 caucvgb 13823 serf0 13824 modfsummods 13930 cvgcmp 13953 mreriincl 15582 acsfn1c 15646 islss4 18263 riinopn 20015 fiinbas 20044 baspartn 20046 isclo2 20181 lmcls 20395 lmcnp 20397 isnrm3 20452 1stcelcls 20553 llyss 20571 nllyss 20572 ptpjpre1 20663 txlly 20728 txnlly 20729 tx1stc 20742 xkococnlem 20751 fbunfip 20962 filssufilg 21004 cnpflf2 21093 fcfnei 21128 isucn2 21372 rescncf 22007 lebnum 22073 cfilss 22318 fgcfil 22319 iscau4 22327 cmetcaulem 22336 cfilres 22344 caussi 22345 ovolunlem1 22528 ulmclm 23421 ulmcaulem 23428 ulmcau 23429 ulmss 23431 rlimcnp 23970 cxploglim 23982 lgsdchr 24355 pntlemp 24527 axcontlem4 25076 usg2wlkeq 25515 3cyclfrgrarn2 25821 nmlnoubi 26518 lnon0 26520 disjpreima 28271 resspos 28495 resstos 28496 submarchi 28577 crefss 28750 iccllyscon 30045 cvmlift2lem1 30097 ss2mcls 30278 mclsax 30279 poimirlem25 32029 poimirlem27 32031 upixp 32120 caushft 32154 sstotbnd3 32172 totbndss 32173 unichnidl 32328 ispridl2 32335 elrfirn2 35609 mzpsubst 35661 eluzrabdioph 35720 fourierdlem103 38185 fourierdlem104 38186 qndenserrnbllem 38275 ralralimp 39134 ewlkle 39811 umgr1wlknloop 39848 |
Copyright terms: Public domain | W3C validator |