![]() |
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 444 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝑥 ∈ 𝐴 → 𝜒)) |
3 | 2 | ralrimiv 2994 | . 2 ⊢ ((𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 𝜒) |
4 | 3 | ex 449 | 1 ⊢ (𝜑 → (𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∈ wcel 2030 ∀wral 2941 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 |
This theorem depends on definitions: df-bi 197 df-an 385 df-ral 2946 |
This theorem is referenced by: ralrimdva 2998 ralrimivv 2999 wefrc 5137 oneqmin 7047 nneneq 8184 cflm 9110 coflim 9121 isf32lem12 9224 axdc3lem2 9311 zorn2lem7 9362 axpre-sup 10028 zmax 11823 zbtwnre 11824 supxrunb2 12188 fzrevral 12463 islss4 19010 topbas 20824 elcls3 20935 neips 20965 clslp 21000 subbascn 21106 cnpnei 21116 comppfsc 21383 fgss2 21725 fbflim2 21828 alexsubALTlem3 21900 alexsubALTlem4 21901 alexsubALT 21902 metcnp3 22392 aalioulem3 24134 brbtwn2 25830 hial0 28087 hial02 28088 ococss 28280 lnopmi 28987 adjlnop 29073 pjss2coi 29151 pj3cor1i 29196 strlem3a 29239 hstrlem3a 29247 mdbr3 29284 mdbr4 29285 dmdmd 29287 dmdbr3 29292 dmdbr4 29293 dmdbr5 29295 ssmd2 29299 mdslmd1i 29316 mdsymlem7 29396 cdj1i 29420 cdj3lem2b 29424 lub0N 34794 glb0N 34798 hlrelat2 35007 snatpsubN 35354 pmaple 35365 pclclN 35495 pclfinN 35504 pclfinclN 35554 ltrneq2 35752 trlval2 35768 trlord 36174 trintALT 39431 lindslinindsimp2 42577 |
Copyright terms: Public domain | W3C validator |