![]() |
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 3137 | . 2 ⊢ ((𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 𝜒) |
4 | 3 | ex 412 | 1 ⊢ (𝜑 → (𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∈ wcel 2098 ∀wral 3053 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 |
This theorem depends on definitions: df-bi 206 df-an 396 df-ral 3054 |
This theorem is referenced by: ralrimdva 3146 ralrimivv 3190 wefrc 5661 oneqmin 7782 nneneq 9206 nneneqOLD 9218 cflm 10242 coflim 10253 isf32lem12 10356 axdc3lem2 10443 zorn2lem7 10494 axpre-sup 11161 zmax 12927 zbtwnre 12928 supxrunb2 13297 fzrevral 13584 lcmfdvdsb 16579 islss4 20801 topbas 22799 elcls3 22911 neips 22941 clslp 22976 subbascn 23082 cnpnei 23092 comppfsc 23360 fgss2 23702 fbflim2 23805 alexsubALTlem3 23877 alexsubALTlem4 23878 alexsubALT 23879 metcnp3 24373 mpomulcn 24709 aalioulem3 26190 brbtwn2 28635 hial0 30827 hial02 30828 ococss 31018 lnopmi 31725 adjlnop 31811 pjss2coi 31889 pj3cor1i 31934 strlem3a 31977 hstrlem3a 31985 mdbr3 32022 mdbr4 32023 dmdmd 32025 dmdbr3 32030 dmdbr4 32031 dmdbr5 32033 ssmd2 32037 mdslmd1i 32054 mdsymlem7 32134 cdj1i 32158 cdj3lem2b 32162 sat1el2xp 34861 fvineqsneu 36783 lub0N 38553 glb0N 38557 hlrelat2 38768 snatpsubN 39115 pmaple 39126 pclclN 39256 pclfinN 39265 pclfinclN 39315 ltrneq2 39513 trlval2 39528 trlord 39934 trintALT 44156 lindslinindsimp2 47357 |
Copyright terms: Public domain | W3C validator |