| 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 456 | . . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒)) |
| 4 | 3 | reximdva 3168 | . 2 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒)) |
| 5 | 1, 4 | mpd 15 | 1 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜒) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∈ wcel 2108 ∃wrex 3070 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-rex 3071 |
| This theorem is referenced by: reximddv3 3172 reximddv2 3215 dedekind 11424 caucvgrlem 15709 isprm5 16744 drsdirfi 18351 sylow2 19644 gexex 19871 nrmsep 23365 regsep2 23384 locfincmp 23534 dissnref 23536 met1stc 24534 xrge0tsms 24856 cnheibor 24987 lmcau 25347 ismbf3d 25689 ulmdvlem3 26445 legov 28593 legtrid 28599 midexlem 28700 opphllem 28743 mideulem 28744 midex 28745 oppperpex 28761 hpgid 28774 lnperpex 28811 trgcopy 28812 grpoidinv 30527 pjhthlem2 31411 mdsymlem3 32424 xrge0tsmsd 33065 isdrng4 33298 drngidl 33461 ssdifidlprm 33486 qsdrngi 33523 ballotlemfc0 34495 ballotlemfcc 34496 cvmliftlem15 35303 unblimceq0 36508 knoppndvlem18 36530 lhpexle3lem 40013 lhpex2leN 40015 cdlemg1cex 40590 fsuppind 42600 nacsfix 42723 unxpwdom3 43107 rfcnnnub 45041 climxrrelem 45764 climxrre 45765 xlimxrre 45846 stoweidlem27 46042 thinciso 49117 |
| Copyright terms: Public domain | W3C validator |