![]() |
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 457 | . . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒)) |
4 | 3 | reximdva 3234 | . 2 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒)) |
5 | 1, 4 | mpd 15 | 1 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∈ wcel 2079 ∃wrex 3104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1775 ax-4 1789 ax-5 1886 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1760 df-ral 3108 df-rex 3109 |
This theorem is referenced by: reximddv2 3238 dedekind 10639 caucvgrlem 14851 isprm5 15868 drsdirfi 17365 sylow2 18469 gexex 18684 nrmsep 21637 regsep2 21656 locfincmp 21806 dissnref 21808 met1stc 22802 xrge0tsms 23113 cnheibor 23230 lmcau 23587 ismbf3d 23926 ulmdvlem3 24661 legov 26041 legtrid 26047 midexlem 26148 opphllem 26191 mideulem 26192 midex 26193 oppperpex 26209 hpgid 26222 lnperpex 26259 trgcopy 26260 grpoidinv 27964 pjhthlem2 28848 mdsymlem3 29861 xrge0tsmsd 30460 ballotlemfc0 31323 ballotlemfcc 31324 cvmliftlem15 32109 unblimceq0 33399 knoppndvlem18 33421 lhpexle3lem 36628 lhpex2leN 36630 cdlemg1cex 37205 nacsfix 38744 unxpwdom3 39131 rfcnnnub 40784 reximddv3 40912 climxrrelem 41526 climxrre 41527 xlimxrre 41608 stoweidlem27 41808 |
Copyright terms: Public domain | W3C validator |