Theorem reximia 3009

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

Syntax hints:   → wi 4   ∈ wcel 1990  ∃wrex 2913

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

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-ral 2917  df-rex 2918

This theorem is referenced by:  reximi  3011  iunpw  6978  wfrdmcl  7423  tz7.49c  7541  fisup2g  8374  fiinf2g  8406  unwdomg  8489  trcl  8604  cfsmolem  9092  1idpr  9851  qmulz  11791  zq  11794  xrsupexmnf  12135  xrinfmexpnf  12136  caubnd2  14097  caurcvg  14407  caurcvg2  14408  caucvg  14409  txlm  21451  norm1exi  28107  chrelat2i  29224  xrofsup  29533  esumcvg  30148  bnj168  30798  poimirlem30  33439  ismblfin  33450  allbutfi  39616  sge0ltfirpmpt  40625  ovolval5lem3  40868  nnsum4primes4  41677  nnsum4primesprm  41679  nnsum4primesgbe  41681  nnsum4primesle9  41683