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 3283 | 1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2110 ∃wrex 3139 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 |
This theorem depends on definitions: df-bi 209 df-an 399 df-ex 1777 df-ral 3143 df-rex 3144 |
This theorem is referenced by: rspcebdv 3617 disjiund 5049 ralxfrd 5301 odi 8199 omeulem1 8202 qsss 8352 findcard3 8755 r1pwss 9207 dfac5lem4 9546 climuni 14903 rlimno1 15004 caurcvg2 15028 sscfn1 17081 gsumval2a 17889 gsumval3 19021 opnnei 21722 dislly 22099 lfinpfin 22126 txcmplem1 22243 ufileu 22521 alexsubALT 22653 metustel 23154 metustfbas 23161 i1faddlem 24288 ulmval 24962 brbtwn 26679 vtxduhgr0nedg 27268 wwlksnredwwlkn0 27668 midwwlks2s3 27725 umgr2cycl 32383 iccllysconn 32492 cvmopnlem 32520 cvmlift2lem10 32554 cvmlift3lem8 32568 sdclem2 35011 heibor1lem 35081 elrfi 39284 eldiophb 39347 dnnumch2 39638 |
Copyright terms: Public domain | W3C validator |