Theorem reximia 3240

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

Syntax hints:   → wi 4   ∈ wcel 2108  ∃wrex 3137

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

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1775  df-ral 3141  df-rex 3142

This theorem is referenced by:  reximi  3241  iunpw  7485  wfrdmcl  7955  tz7.49c  8074  fisup2g  8924  fiinf2g  8956  unwdomg  9040  trcl  9162  cfsmolem  9684  1idpr  10443  qmulz  12343  xrsupexmnf  12690  xrinfmexpnf  12691  caubnd2  14709  caurcvg  15025  caurcvg2  15026  caucvg  15027  sgrpidmnd  17908  txlm  22248  norm1exi  29019  chrelat2i  30134  xrofsup  30484  esumcvg  31338  bnj168  31993  satfv1  32603  satfv0fvfmla0  32653  poimirlem30  34914  ismblfin  34925  dffltz  39261  allbutfi  41654  sge0ltfirpmpt  42680  ovolval5lem3  42926  2reu8i  43302  nnsum4primes4  43944  nnsum4primesprm  43946  nnsum4primesgbe  43948  nnsum4primesle9  43950