![]() |
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 567 | . 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → (𝑥 ∈ 𝐴 ∧ 𝜓)) |
3 | 2 | reximi2 3068 | 1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2098 ∃wrex 3059 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1774 df-rex 3060 |
This theorem is referenced by: reximi 3073 iunpw 7774 wfrdmclOLD 8338 tz7.49c 8467 fisup2g 9493 fiinf2g 9525 unwdomg 9609 trcl 9753 cfsmolem 10295 1idpr 11054 qmulz 12968 xrsupexmnf 13319 xrinfmexpnf 13320 caubnd2 15340 caurcvg 15659 caurcvg2 15660 caucvg 15661 sgrpidmnd 18702 txlm 23596 znegscl 28289 norm1exi 31132 chrelat2i 32247 xrofsup 32619 esumcvg 33836 bnj168 34492 satfv1 35104 satfv0fvfmla0 35154 poimirlem30 37254 ismblfin 37265 dffltz 42193 allbutfi 44913 sge0ltfirpmpt 45934 ovolval5lem3 46180 2reu8i 46631 nnsum4primes4 47266 nnsum4primesprm 47268 nnsum4primesgbe 47270 nnsum4primesle9 47272 0aryfvalelfv 47894 |
Copyright terms: Public domain | W3C validator |