![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rexlimdvw | Structured version Visualization version GIF version |
Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 18-Jun-2014.) |
Ref | Expression |
---|---|
rexlimdvw.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
Ref | Expression |
---|---|
rexlimdvw | ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rexlimdvw.1 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
2 | 1 | a1d 25 | . 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒))) |
3 | 2 | rexlimdv 3143 | 1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2099 ∃wrex 3060 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1775 df-rex 3061 |
This theorem is referenced by: rspcebdv 3602 disjiund 5143 ralxfrd 5412 poxp3 8164 odi 8609 omeulem1 8612 qsss 8807 findcard3 9319 findcard3OLD 9320 ttrclselem2 9769 r1pwss 9827 dfac5lem4 10169 climuni 15554 rlimno1 15658 caurcvg2 15682 sscfn1 17833 gsumval2a 18678 gsumval3 19905 opnnei 23115 dislly 23492 lfinpfin 23519 txcmplem1 23636 ufileu 23914 alexsubALT 24046 metustel 24550 metustfbas 24557 i1faddlem 25713 ulmval 26409 brbtwn 28833 vtxduhgr0nedg 29429 wwlksnredwwlkn0 29830 midwwlks2s3 29886 umgr2cycl 34969 iccllysconn 35078 cvmopnlem 35106 cvmlift2lem10 35140 cvmlift3lem8 35154 sdclem2 37443 heibor1lem 37510 elrfi 42351 eldiophb 42414 dnnumch2 42706 |
Copyright terms: Public domain | W3C validator |