Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > reximddv | Structured version Visualization version GIF version |
Description: Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by Thierry Arnoux, 7-Dec-2016.) |
Ref | Expression |
---|---|
reximddva.1 | ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝜓)) → 𝜒) |
reximddva.2 | ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓) |
Ref | Expression |
---|---|
reximddv | ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | reximddva.2 | . 2 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓) | |
2 | reximddva.1 | . . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝜓)) → 𝜒) | |
3 | 2 | expr 459 | . . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒)) |
4 | 3 | reximdva 3276 | . 2 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒)) |
5 | 1, 4 | mpd 15 | 1 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 ∈ wcel 2114 ∃wrex 3141 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 |
This theorem depends on definitions: df-bi 209 df-an 399 df-ex 1781 df-ral 3145 df-rex 3146 |
This theorem is referenced by: reximddv2 3280 dedekind 10805 caucvgrlem 15031 isprm5 16053 drsdirfi 17550 sylow2 18753 gexex 18975 nrmsep 21967 regsep2 21986 locfincmp 22136 dissnref 22138 met1stc 23133 xrge0tsms 23444 cnheibor 23561 lmcau 23918 ismbf3d 24257 ulmdvlem3 24992 legov 26373 legtrid 26379 midexlem 26480 opphllem 26523 mideulem 26524 midex 26525 oppperpex 26541 hpgid 26554 lnperpex 26591 trgcopy 26592 grpoidinv 28287 pjhthlem2 29171 mdsymlem3 30184 xrge0tsmsd 30694 ballotlemfc0 31752 ballotlemfcc 31753 cvmliftlem15 32547 unblimceq0 33848 knoppndvlem18 33870 lhpexle3lem 37149 lhpex2leN 37151 cdlemg1cex 37726 nacsfix 39316 unxpwdom3 39702 rfcnnnub 41300 reximddv3 41427 climxrrelem 42037 climxrre 42038 xlimxrre 42119 stoweidlem27 42319 |
Copyright terms: Public domain | W3C validator |