Theorem reximia 2992

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

Syntax hints:   → wi 4   ∈ wcel 1977  ∃wrex 2897

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

This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-ral 2901  df-rex 2902

This theorem is referenced by:  reximi  2994  iunpw  6870  wfrdmcl  7310  tz7.49c  7428  fisup2g  8257  fiinf2g  8289  unwdomg  8372  trcl  8487  cfsmolem  8975  1idpr  9730  qmulz  11667  zq  11670  xrsupexmnf  12007  xrinfmexpnf  12008  caubnd2  13945  caurcvg  14255  caurcvg2  14256  caucvg  14257  txlm  21261  norm1exi  27491  chrelat2i  28608  xrofsup  28923  esumcvg  29475  bnj168  30052  poimirlem30  32609  ismblfin  32620  allbutfi  38557  sge0ltfirpmpt  39301  ovolval5lem3  39544  nnsum4primes4  40205  nnsum4primesprm  40207  nnsum4primesgbe  40209  nnsum4primesle9  40211