| 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 3153 | 1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∈ wcel 2108 ∃wrex 3070 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-rex 3071 |
| This theorem is referenced by: rspcebdv 3616 disjiund 5134 ralxfrd 5408 poxp3 8175 odi 8617 omeulem1 8620 qsss 8818 findcard3 9318 findcard3OLD 9319 ttrclselem2 9766 r1pwss 9824 dfac5lem4 10166 dfac5lem4OLD 10168 climuni 15588 rlimno1 15690 caurcvg2 15714 sscfn1 17861 gsumval2a 18698 gsumval3 19925 opnnei 23128 dislly 23505 lfinpfin 23532 txcmplem1 23649 ufileu 23927 alexsubALT 24059 metustel 24563 metustfbas 24570 i1faddlem 25728 ulmval 26423 brbtwn 28914 vtxduhgr0nedg 29510 wwlksnredwwlkn0 29916 midwwlks2s3 29972 umgr2cycl 35146 iccllysconn 35255 cvmopnlem 35283 cvmlift2lem10 35317 cvmlift3lem8 35331 sdclem2 37749 heibor1lem 37816 elrfi 42705 eldiophb 42768 dnnumch2 43057 |
| Copyright terms: Public domain | W3C validator |