![]() |
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 449 | . . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒)) |
4 | 3 | reximdva 3197 | . 2 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒)) |
5 | 1, 4 | mpd 15 | 1 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 385 ∈ wcel 2157 ∃wrex 3090 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 |
This theorem depends on definitions: df-bi 199 df-an 386 df-ex 1876 df-ral 3094 df-rex 3095 |
This theorem is referenced by: reximddv2 3201 dedekind 10490 caucvgrlem 14744 isprm5 15752 drsdirfi 17253 sylow2 18354 gexex 18571 nrmsep 21490 regsep2 21509 locfincmp 21658 dissnref 21660 met1stc 22654 xrge0tsms 22965 cnheibor 23082 lmcau 23439 ismbf3d 23762 ulmdvlem3 24497 legov 25836 legtrid 25842 midexlem 25943 opphllem 25983 mideulem 25984 midex 25985 oppperpex 26001 hpgid 26014 lnperpex 26051 trgcopy 26052 grpoidinv 27888 pjhthlem2 28776 mdsymlem3 29789 xrge0tsmsd 30301 ballotlemfc0 31071 ballotlemfcc 31072 cvmliftlem15 31797 unblimceq0 33006 knoppndvlem18 33028 lhpexle3lem 36032 lhpex2leN 36034 cdlemg1cex 36609 nacsfix 38057 unxpwdom3 38446 rfcnnnub 39951 reximddv3 40094 climxrrelem 40721 climxrre 40722 xlimxrre 40797 stoweidlem27 40983 |
Copyright terms: Public domain | W3C validator |