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 2948 | . 2 ⊢ ((𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 𝜒) |
4 | 3 | ex 449 | 1 ⊢ (𝜑 → (𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∈ wcel 1977 ∀wral 2896 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 |
This theorem depends on definitions: df-bi 196 df-an 385 df-ral 2901 |
This theorem is referenced by: ralrimdva 2952 ralrimivv 2953 wefrc 5032 oneqmin 6897 nneneq 8028 cflm 8955 coflim 8966 isf32lem12 9069 axdc3lem2 9156 zorn2lem7 9207 axpre-sup 9869 zmax 11661 zbtwnre 11662 supxrunb2 12022 fzrevral 12294 islss4 18783 topbas 20587 elcls3 20697 neips 20727 clslp 20762 subbascn 20868 cnpnei 20878 comppfsc 21145 fgss2 21488 fbflim2 21591 alexsubALTlem3 21663 alexsubALTlem4 21664 alexsubALT 21665 metcnp3 22155 aalioulem3 23893 brbtwn2 25585 hial0 27343 hial02 27344 ococss 27536 lnopmi 28243 adjlnop 28329 pjss2coi 28407 pj3cor1i 28452 strlem3a 28495 hstrlem3a 28503 mdbr3 28540 mdbr4 28541 dmdmd 28543 dmdbr3 28548 dmdbr4 28549 dmdbr5 28551 ssmd2 28555 mdslmd1i 28572 mdsymlem7 28652 cdj1i 28676 cdj3lem2b 28680 lub0N 33494 glb0N 33498 hlrelat2 33707 snatpsubN 34054 pmaple 34065 pclclN 34195 pclfinN 34204 pclfinclN 34254 ltrneq2 34452 trlval2 34468 trlord 34875 trintALT 38139 lindslinindsimp2 42046 |
Copyright terms: Public domain | W3C validator |