| 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 406 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝑥 ∈ 𝐴 → 𝜒)) |
| 3 | 2 | ralrimiv 3145 | . 2 ⊢ ((𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 𝜒) |
| 4 | 3 | ex 412 | 1 ⊢ (𝜑 → (𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∈ 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: ralrimdva 3154 ralrimivv 3200 wefrc 5679 oneqmin 7820 nneneq 9246 nneneqOLD 9258 cflm 10290 coflim 10301 isf32lem12 10404 axdc3lem2 10491 zorn2lem7 10542 axpre-sup 11209 zmax 12987 zbtwnre 12988 supxrunb2 13362 fzrevral 13652 lcmfdvdsb 16680 islss4 20960 topbas 22979 elcls3 23091 neips 23121 clslp 23156 subbascn 23262 cnpnei 23272 comppfsc 23540 fgss2 23882 fbflim2 23985 alexsubALTlem3 24057 alexsubALTlem4 24058 alexsubALT 24059 metcnp3 24553 mpomulcn 24891 aalioulem3 26376 brbtwn2 28920 hial0 31121 hial02 31122 ococss 31312 lnopmi 32019 adjlnop 32105 pjss2coi 32183 pj3cor1i 32228 strlem3a 32271 hstrlem3a 32279 mdbr3 32316 mdbr4 32317 dmdmd 32319 dmdbr3 32324 dmdbr4 32325 dmdbr5 32327 ssmd2 32331 mdslmd1i 32348 mdsymlem7 32428 cdj1i 32452 cdj3lem2b 32456 sat1el2xp 35384 fvineqsneu 37412 lub0N 39190 glb0N 39194 hlrelat2 39405 snatpsubN 39752 pmaple 39763 pclclN 39893 pclfinN 39902 pclfinclN 39952 ltrneq2 40150 trlval2 40165 trlord 40571 trintALT 44901 lindslinindsimp2 48380 |
| Copyright terms: Public domain | W3C validator |