![]() |
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.) |
Ref | Expression |
---|---|
reximia.1 | ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) |
Ref | Expression |
---|---|
reximia | ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rexim 3217 | . 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓)) | |
2 | reximia.1 | . 2 ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) | |
3 | 1, 2 | mprg 3136 | 1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2166 ∃wrex 3119 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 |
This theorem depends on definitions: df-bi 199 df-an 387 df-ex 1881 df-ral 3123 df-rex 3124 |
This theorem is referenced by: reximi 3220 iunpw 7240 wfrdmcl 7690 tz7.49c 7808 fisup2g 8644 fiinf2g 8676 unwdomg 8759 trcl 8882 cfsmolem 9408 1idpr 10167 qmulz 12075 zq 12078 xrsupexmnf 12424 xrinfmexpnf 12425 caubnd2 14475 caurcvg 14785 caurcvg2 14786 caucvg 14787 txlm 21823 norm1exi 28663 chrelat2i 29780 xrofsup 30081 esumcvg 30694 bnj168 31346 poimirlem30 33984 ismblfin 33995 dffltz 38098 allbutfi 40412 sge0ltfirpmpt 41417 ovolval5lem3 41663 nnsum4primes4 42508 nnsum4primesprm 42510 nnsum4primesgbe 42512 nnsum4primesle9 42514 |
Copyright terms: Public domain | W3C validator |