| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > reximia | Structured version Visualization version GIF version | ||
| Description: Inference quantifying both antecedent and consequent. (Contributed by NM, 10-Feb-1997.) (Proof shortened by Wolf Lammen, 31-Oct-2024.) |
| Ref | Expression |
|---|---|
| ralimia.1 | ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) |
| Ref | Expression |
|---|---|
| reximia | ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ralimia.1 | . . 3 ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) | |
| 2 | 1 | imdistani 568 | . 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → (𝑥 ∈ 𝐴 ∧ 𝜓)) |
| 3 | 2 | reximi2 3079 | 1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∈ 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 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-rex 3071 |
| This theorem is referenced by: reximi 3084 iunpw 7791 wfrdmclOLD 8357 tz7.49c 8486 fisup2g 9508 fiinf2g 9540 unwdomg 9624 trcl 9768 cfsmolem 10310 1idpr 11069 qmulz 12993 xrsupexmnf 13347 xrinfmexpnf 13348 caubnd2 15396 caurcvg 15713 caurcvg2 15714 caucvg 15715 sgrpidmnd 18752 txlm 23656 znegscl 28378 norm1exi 31269 chrelat2i 32384 xrofsup 32771 esumcvg 34087 bnj168 34744 satfv1 35368 satfv0fvfmla0 35418 poimirlem30 37657 ismblfin 37668 dffltz 42644 allbutfi 45404 sge0ltfirpmpt 46423 ovolval5lem3 46669 2reu8i 47125 nnsum4primes4 47776 nnsum4primesprm 47778 nnsum4primesgbe 47780 nnsum4primesle9 47782 0aryfvalelfv 48556 |
| Copyright terms: Public domain | W3C validator |