![]() |
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 410 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝑥 ∈ 𝐴 → 𝜒)) |
3 | 2 | ralrimiv 3148 | . 2 ⊢ ((𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 𝜒) |
4 | 3 | ex 416 | 1 ⊢ (𝜑 → (𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∈ wcel 2111 ∀wral 3106 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ral 3111 |
This theorem is referenced by: ralrimdva 3154 ralrimivv 3155 wefrc 5513 oneqmin 7500 nneneq 8684 cflm 9661 coflim 9672 isf32lem12 9775 axdc3lem2 9862 zorn2lem7 9913 axpre-sup 10580 zmax 12333 zbtwnre 12334 supxrunb2 12701 fzrevral 12987 lcmfdvdsb 15977 islss4 19727 topbas 21577 elcls3 21688 neips 21718 clslp 21753 subbascn 21859 cnpnei 21869 comppfsc 22137 fgss2 22479 fbflim2 22582 alexsubALTlem3 22654 alexsubALTlem4 22655 alexsubALT 22656 metcnp3 23147 aalioulem3 24930 brbtwn2 26699 hial0 28885 hial02 28886 ococss 29076 lnopmi 29783 adjlnop 29869 pjss2coi 29947 pj3cor1i 29992 strlem3a 30035 hstrlem3a 30043 mdbr3 30080 mdbr4 30081 dmdmd 30083 dmdbr3 30088 dmdbr4 30089 dmdbr5 30091 ssmd2 30095 mdslmd1i 30112 mdsymlem7 30192 cdj1i 30216 cdj3lem2b 30220 sat1el2xp 32739 fvineqsneu 34828 lub0N 36485 glb0N 36489 hlrelat2 36699 snatpsubN 37046 pmaple 37057 pclclN 37187 pclfinN 37196 pclfinclN 37246 ltrneq2 37444 trlval2 37459 trlord 37865 trintALT 41587 lindslinindsimp2 44872 |
Copyright terms: Public domain | W3C validator |