Theorem reximia 3205

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 3204	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓))
2		reximia.1	. 2 ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))
3	1, 2	mprg 3120	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ∈ wcel 2111  ∃wrex 3107

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

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-ral 3111  df-rex 3112

This theorem is referenced by:  reximi  3206  iunpw  7473  wfrdmcl  7946  tz7.49c  8065  fisup2g  8916  fiinf2g  8948  unwdomg  9032  trcl  9154  cfsmolem  9681  1idpr  10440  qmulz  12339  xrsupexmnf  12686  xrinfmexpnf  12687  caubnd2  14709  caurcvg  15025  caurcvg2  15026  caucvg  15027  sgrpidmnd  17908  txlm  22253  norm1exi  29033  chrelat2i  30148  xrofsup  30518  esumcvg  31455  bnj168  32110  satfv1  32723  satfv0fvfmla0  32773  poimirlem30  35087  ismblfin  35098  dffltz  39615  allbutfi  42029  sge0ltfirpmpt  43047  ovolval5lem3  43293  2reu8i  43669  nnsum4primes4  44307  nnsum4primesprm  44309  nnsum4primesgbe  44311  nnsum4primesle9  44313  0aryfvalelfv  45049