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 3012 | 1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 1977 ∃wrex 2897 |
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-ex 1696 df-ral 2901 df-rex 2902 |
This theorem is referenced by: ralxfrd 4805 odi 7546 omeulem1 7549 qsss 7695 findcard3 8088 r1pwss 8530 dfac5lem4 8832 climuni 14131 rlimno1 14232 caurcvg2 14256 sscfn1 16300 gsumval2a 17102 gsumval3 18131 opnnei 20734 dislly 21110 lfinpfin 21137 txcmplem1 21254 ufileu 21533 alexsubALT 21665 metustel 22165 metustfbas 22172 i1faddlem 23266 ulmval 23938 brbtwn 25579 wwlknredwwlkn0 26255 iseupa 26492 iccllyscon 30486 cvmopnlem 30514 cvmlift2lem10 30548 cvmlift3lem8 30562 sdclem2 32708 heibor1lem 32778 elrfi 36275 eldiophb 36338 dnnumch2 36633 vtxduhgr0nedg 40707 wwlksnredwwlkn0 41102 elwwlks2ons3 41159 clwwlksnun 41281 |
Copyright terms: Public domain | W3C validator |