![]() |
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 398 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝑥 ∈ 𝐴 → 𝜒)) |
3 | 2 | ralrimiv 3131 | . 2 ⊢ ((𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 𝜒) |
4 | 3 | ex 405 | 1 ⊢ (𝜑 → (𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 387 ∈ wcel 2050 ∀wral 3088 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 |
This theorem depends on definitions: df-bi 199 df-an 388 df-ral 3093 |
This theorem is referenced by: ralrimdva 3139 ralrimivv 3140 wefrc 5402 oneqmin 7338 nneneq 8498 cflm 9472 coflim 9483 isf32lem12 9586 axdc3lem2 9673 zorn2lem7 9724 axpre-sup 10391 zmax 12162 zbtwnre 12163 supxrunb2 12532 fzrevral 12811 lcmfdvdsb 15846 islss4 19459 topbas 21287 elcls3 21398 neips 21428 clslp 21463 subbascn 21569 cnpnei 21579 comppfsc 21847 fgss2 22189 fbflim2 22292 alexsubALTlem3 22364 alexsubALTlem4 22365 alexsubALT 22366 metcnp3 22856 aalioulem3 24629 brbtwn2 26397 hial0 28661 hial02 28662 ococss 28854 lnopmi 29561 adjlnop 29647 pjss2coi 29725 pj3cor1i 29770 strlem3a 29813 hstrlem3a 29821 mdbr3 29858 mdbr4 29859 dmdmd 29861 dmdbr3 29866 dmdbr4 29867 dmdbr5 29869 ssmd2 29873 mdslmd1i 29890 mdsymlem7 29970 cdj1i 29994 cdj3lem2b 29998 sat1el2xp 32189 fvineqsneu 34133 lub0N 35770 glb0N 35774 hlrelat2 35984 snatpsubN 36331 pmaple 36342 pclclN 36472 pclfinN 36481 pclfinclN 36531 ltrneq2 36729 trlval2 36744 trlord 37150 trintALT 40634 lindslinindsimp2 43886 |
Copyright terms: Public domain | W3C validator |