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 643 | . . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒)) |
4 | 3 | reximdva 3017 | . 2 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒)) |
5 | 1, 4 | mpd 15 | 1 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 384 ∈ wcel 1990 ∃wrex 2913 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 |
This theorem depends on definitions: df-bi 197 df-an 386 df-ex 1705 df-ral 2917 df-rex 2918 |
This theorem is referenced by: reximddv2 3020 dedekind 10200 caucvgrlem 14403 isprm5 15419 drsdirfi 16938 sylow2 18041 gexex 18256 nrmsep 21161 regsep2 21180 locfincmp 21329 dissnref 21331 met1stc 22326 xrge0tsms 22637 cnheibor 22754 lmcau 23111 ismbf3d 23421 ulmdvlem3 24156 legov 25480 legtrid 25486 midexlem 25587 opphllem 25627 mideulem 25628 midex 25629 oppperpex 25645 hpgid 25658 lnperpex 25695 trgcopy 25696 grpoidinv 27362 pjhthlem2 28251 mdsymlem3 29264 xrge0tsmsd 29785 ballotlemfc0 30554 ballotlemfcc 30555 cvmliftlem15 31280 unblimceq0 32498 knoppndvlem18 32520 lhpexle3lem 35297 lhpex2leN 35299 cdlemg1cex 35876 nacsfix 37275 unxpwdom3 37665 rfcnnnub 39195 reximddv3 39343 climxrrelem 39981 climxrre 39982 xlimxrre 40057 stoweidlem27 40244 |
Copyright terms: Public domain | W3C validator |