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 409 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝑥 ∈ 𝐴 → 𝜒)) |
3 | 2 | ralrimiv 3183 | . 2 ⊢ ((𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 𝜒) |
4 | 3 | ex 415 | 1 ⊢ (𝜑 → (𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 ∈ wcel 2114 ∀wral 3140 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 |
This theorem depends on definitions: df-bi 209 df-an 399 df-ral 3145 |
This theorem is referenced by: ralrimdva 3191 ralrimivv 3192 wefrc 5551 oneqmin 7522 nneneq 8702 cflm 9674 coflim 9685 isf32lem12 9788 axdc3lem2 9875 zorn2lem7 9926 axpre-sup 10593 zmax 12348 zbtwnre 12349 supxrunb2 12716 fzrevral 12995 lcmfdvdsb 15989 islss4 19736 topbas 21582 elcls3 21693 neips 21723 clslp 21758 subbascn 21864 cnpnei 21874 comppfsc 22142 fgss2 22484 fbflim2 22587 alexsubALTlem3 22659 alexsubALTlem4 22660 alexsubALT 22661 metcnp3 23152 aalioulem3 24925 brbtwn2 26693 hial0 28881 hial02 28882 ococss 29072 lnopmi 29779 adjlnop 29865 pjss2coi 29943 pj3cor1i 29988 strlem3a 30031 hstrlem3a 30039 mdbr3 30076 mdbr4 30077 dmdmd 30079 dmdbr3 30084 dmdbr4 30085 dmdbr5 30087 ssmd2 30091 mdslmd1i 30108 mdsymlem7 30188 cdj1i 30212 cdj3lem2b 30216 sat1el2xp 32628 fvineqsneu 34694 lub0N 36327 glb0N 36331 hlrelat2 36541 snatpsubN 36888 pmaple 36899 pclclN 37029 pclfinN 37038 pclfinclN 37088 ltrneq2 37286 trlval2 37301 trlord 37707 trintALT 41222 lindslinindsimp2 44525 |
Copyright terms: Public domain | W3C validator |