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 1729). (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 2945 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ 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: poss 4961 sess1 5006 sess2 5007 riinint 5303 iinpreima 6253 dffo4 6283 dffo5 6284 isoini2 6489 tfindsg 6952 el2mpt2csbcl 7137 iiner 7706 xpf1o 8007 dffi3 8220 brwdom3 8370 xpwdomg 8373 bndrank 8587 cfub 8954 cff1 8963 cfflb 8964 cfslb2n 8973 cofsmo 8974 cfcoflem 8977 pwcfsdom 9284 fpwwe2lem13 9343 inawinalem 9390 grupr 9498 fsequb 12636 cau3lem 13942 caubnd2 13945 caubnd 13946 rlim2lt 14076 rlim3 14077 climshftlem 14153 isercolllem1 14243 climcau 14249 caucvgb 14258 serf0 14259 modfsummods 14366 cvgcmp 14389 mreriincl 16081 acsfn1c 16146 islss4 18783 riinopn 20538 fiinbas 20567 baspartn 20569 isclo2 20702 lmcls 20916 lmcnp 20918 isnrm3 20973 1stcelcls 21074 llyss 21092 nllyss 21093 ptpjpre1 21184 txlly 21249 txnlly 21250 tx1stc 21263 xkococnlem 21272 fbunfip 21483 filssufilg 21525 cnpflf2 21614 fcfnei 21649 isucn2 21893 rescncf 22508 lebnum 22571 cfilss 22876 fgcfil 22877 iscau4 22885 cmetcaulem 22894 cfilres 22902 caussi 22903 ovolunlem1 23072 ulmclm 23945 ulmcaulem 23952 ulmcau 23953 ulmss 23955 rlimcnp 24492 cxploglim 24504 lgsdchr 24880 pntlemp 25099 axcontlem4 25647 usg2wlkeq 26236 3cyclfrgrarn2 26541 nmlnoubi 27035 lnon0 27037 disjpreima 28779 resspos 28990 resstos 28991 submarchi 29071 crefss 29244 iccllyscon 30486 cvmlift2lem1 30538 ss2mcls 30719 mclsax 30720 poimirlem25 32604 poimirlem27 32606 upixp 32694 caushft 32727 sstotbnd3 32745 totbndss 32746 unichnidl 33000 ispridl2 33007 elrfirn2 36277 mzpsubst 36329 eluzrabdioph 36388 neik0pk1imk0 37365 fourierdlem103 39102 fourierdlem104 39103 qndenserrnbllem 39190 ralralimp 40309 ewlkle 40807 uspgr2wlkeq 40854 umgr1wlknloop 40857 1wlkiswwlksupgr2 41074 3cyclfrgrrn2 41457 |
Copyright terms: Public domain | W3C validator |