Theorem reximia 3155

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

Syntax hints:   → wi 4   ∈ wcel 2155  ∃wrex 3056

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

This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1875  df-ral 3060  df-rex 3061

This theorem is referenced by:  reximi  3157  iunpw  7176  wfrdmcl  7627  tz7.49c  7745  fisup2g  8581  fiinf2g  8613  unwdomg  8696  trcl  8819  cfsmolem  9345  1idpr  10104  qmulz  11992  zq  11995  xrsupexmnf  12337  xrinfmexpnf  12338  caubnd2  14382  caurcvg  14692  caurcvg2  14693  caucvg  14694  txlm  21731  norm1exi  28563  chrelat2i  29680  xrofsup  29982  esumcvg  30595  bnj168  31247  poimirlem30  33863  ismblfin  33874  allbutfi  40253  sge0ltfirpmpt  41262  ovolval5lem3  41508  nnsum4primes4  42353  nnsum4primesprm  42355  nnsum4primesgbe  42357  nnsum4primesle9  42359