![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ralrimdv | Structured version Visualization version GIF version |
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 27-May-1998.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 28-Dec-2019.) |
Ref | Expression |
---|---|
ralrimdv.1 | ⊢ (𝜑 → (𝜓 → (𝑥 ∈ 𝐴 → 𝜒))) |
Ref | Expression |
---|---|
ralrimdv | ⊢ (𝜑 → (𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralrimdv.1 | . . . 4 ⊢ (𝜑 → (𝜓 → (𝑥 ∈ 𝐴 → 𝜒))) | |
2 | 1 | imp 408 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝑥 ∈ 𝐴 → 𝜒)) |
3 | 2 | ralrimiv 3139 | . 2 ⊢ ((𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 𝜒) |
4 | 3 | ex 414 | 1 ⊢ (𝜑 → (𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 ∈ wcel 2107 ∀wral 3061 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ral 3062 |
This theorem is referenced by: ralrimdva 3148 ralrimivv 3192 wefrc 5628 oneqmin 7736 nneneq 9156 nneneqOLD 9168 cflm 10191 coflim 10202 isf32lem12 10305 axdc3lem2 10392 zorn2lem7 10443 axpre-sup 11110 zmax 12875 zbtwnre 12876 supxrunb2 13245 fzrevral 13532 lcmfdvdsb 16524 islss4 20438 topbas 22338 elcls3 22450 neips 22480 clslp 22515 subbascn 22621 cnpnei 22631 comppfsc 22899 fgss2 23241 fbflim2 23344 alexsubALTlem3 23416 alexsubALTlem4 23417 alexsubALT 23418 metcnp3 23912 aalioulem3 25710 brbtwn2 27896 hial0 30086 hial02 30087 ococss 30277 lnopmi 30984 adjlnop 31070 pjss2coi 31148 pj3cor1i 31193 strlem3a 31236 hstrlem3a 31244 mdbr3 31281 mdbr4 31282 dmdmd 31284 dmdbr3 31289 dmdbr4 31290 dmdbr5 31292 ssmd2 31296 mdslmd1i 31313 mdsymlem7 31393 cdj1i 31417 cdj3lem2b 31421 sat1el2xp 34030 fvineqsneu 35928 lub0N 37697 glb0N 37701 hlrelat2 37912 snatpsubN 38259 pmaple 38270 pclclN 38400 pclfinN 38409 pclfinclN 38459 ltrneq2 38657 trlval2 38672 trlord 39078 trintALT 43251 lindslinindsimp2 46630 |
Copyright terms: Public domain | W3C validator |