Theorem reximia 3244

Description: Inference quantifying both antecedent and consequent. (Contributed by NM, 10-Feb-1997.)

Hypothesis

Ref	Expression
reximia.1	⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))

Assertion

Ref	Expression
reximia	⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓)

Proof of Theorem reximia

Step	Hyp	Ref	Expression
1		rexim 3243	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓))
2		reximia.1	. 2 ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))
3	1, 2	mprg 3154	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ∈ wcel 2114  ∃wrex 3141

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-ral 3145  df-rex 3146

This theorem is referenced by:  reximi  3245  iunpw  7495  wfrdmcl  7965  tz7.49c  8084  fisup2g  8934  fiinf2g  8966  unwdomg  9050  trcl  9172  cfsmolem  9694  1idpr  10453  qmulz  12354  xrsupexmnf  12701  xrinfmexpnf  12702  caubnd2  14719  caurcvg  15035  caurcvg2  15036  caucvg  15037  sgrpidmnd  17918  txlm  22258  norm1exi  29029  chrelat2i  30144  xrofsup  30494  esumcvg  31347  bnj168  32002  satfv1  32612  satfv0fvfmla0  32662  poimirlem30  34924  ismblfin  34935  dffltz  39278  allbutfi  41672  sge0ltfirpmpt  42697  ovolval5lem3  42943  2reu8i  43319  nnsum4primes4  43961  nnsum4primesprm  43963  nnsum4primesgbe  43965  nnsum4primesle9  43967