| 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 3167 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∈ wcel 2108 ∀wral 3061 |
| 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 3062 |
| This theorem is referenced by: r19.21v 3180 ss2ralv 4054 poss 5594 sess1 5650 sess2 5651 riinint 5982 iinpreima 7089 dffo4 7123 dffo5 7124 isoini2 7359 tfindsg 7882 el2mpocsbcl 8110 xpord3inddlem 8179 iiner 8829 xpf1o 9179 dffi3 9471 brwdom3 9622 xpwdomg 9625 ttrclss 9760 bndrank 9881 cfub 10289 cff1 10298 cfflb 10299 cfslb2n 10308 cofsmo 10309 cfcoflem 10312 pwcfsdom 10623 fpwwe2lem12 10682 inawinalem 10729 grupr 10837 fsequb 14016 cau3lem 15393 caubnd2 15396 caubnd 15397 rlim2lt 15533 rlim3 15534 climshftlem 15610 climcau 15707 caucvgb 15716 serf0 15717 modfsummods 15829 cvgcmp 15852 mreriincl 17641 acsfn1c 17705 islss4 20960 riinopn 22914 fiinbas 22959 baspartn 22961 isclo2 23096 lmcls 23310 lmcnp 23312 isnrm3 23367 1stcelcls 23469 llyss 23487 nllyss 23488 ptpjpre1 23579 txlly 23644 txnlly 23645 tx1stc 23658 xkococnlem 23667 fbunfip 23877 filssufilg 23919 cnpflf2 24008 fcfnei 24043 isucn2 24288 rescncf 24923 lebnum 24996 cfilss 25304 fgcfil 25305 iscau4 25313 cmetcaulem 25322 caussi 25331 ovolunlem1 25532 ulmclm 26430 ulmcaulem 26437 ulmcau 26438 ulmss 26440 rlimcnp 27008 cxploglim 27021 2sqreunnlem2 27499 pntlemp 27654 nosupno 27748 nosupres 27752 noinfno 27763 noinfres 27767 sssslt2 27841 madebdayim 27926 madebdaylemold 27936 axcontlem4 28982 ewlkle 29623 uspgr2wlkeq 29664 umgrwlknloop 29667 wlkiswwlksupgr2 29897 3cyclfrgrrn2 30306 nmlnoubi 30815 lnon0 30817 disjpreima 32597 resspos 32956 resstos 32957 submarchi 33193 prmidl2 33469 crefss 33848 iccllysconn 35255 cvmlift2lem1 35307 dmopab3rexdif 35410 ss2mcls 35573 mclsax 35574 isinf2 37406 poimirlem25 37652 poimirlem27 37654 upixp 37736 caushft 37768 sstotbnd3 37783 totbndss 37784 unichnidl 38038 ispridl2 38045 elrfirn2 42707 mzpsubst 42759 eluzrabdioph 42817 neik0pk1imk0 44060 mnuop3d 44290 ismnushort 44320 pwclaxpow 45001 limsupub 45719 limsupre3lem 45747 climuzlem 45758 xlimbr 45842 fourierdlem103 46224 fourierdlem104 46225 qndenserrnbllem 46309 2reuimp 47127 ralralimp 47290 |
| Copyright terms: Public domain | W3C validator |