Theorem reximia 3218

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

Syntax hints:   → wi 4   ∈ wcel 2166  ∃wrex 3119

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

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1881  df-ral 3123  df-rex 3124

This theorem is referenced by:  reximi  3220  iunpw  7240  wfrdmcl  7690  tz7.49c  7808  fisup2g  8644  fiinf2g  8676  unwdomg  8759  trcl  8882  cfsmolem  9408  1idpr  10167  qmulz  12075  zq  12078  xrsupexmnf  12424  xrinfmexpnf  12425  caubnd2  14475  caurcvg  14785  caurcvg2  14786  caucvg  14787  txlm  21823  norm1exi  28663  chrelat2i  29780  xrofsup  30081  esumcvg  30694  bnj168  31346  poimirlem30  33984  ismblfin  33995  dffltz  38098  allbutfi  40412  sge0ltfirpmpt  41417  ovolval5lem3  41663  nnsum4primes4  42508  nnsum4primesprm  42510  nnsum4primesgbe  42512  nnsum4primesle9  42514