Theorem reximia 3174

Description: Inference quantifying both antecedent and consequent. (Contributed by NM, 10-Feb-1997.) (Proof shortened by Wolf Lammen, 31-Oct-2024.)

Hypothesis

Ref	Expression
reximia.1	⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))

Assertion

Ref	Expression
reximia	⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓)

Proof of Theorem reximia

Step	Hyp	Ref	Expression
1		reximia.1	. . 3 ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))
2	1	imdistani 568	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → (𝑥 ∈ 𝐴 ∧ 𝜓))
3	2	reximi2 3173	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ∈ wcel 2109  ∃wrex 3066

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

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1786  df-rex 3071

This theorem is referenced by:  reximi  3176  iunpw  7612  wfrdmclOLD  8132  tz7.49c  8261  fisup2g  9188  fiinf2g  9220  unwdomg  9304  trcl  9469  cfsmolem  10010  1idpr  10769  qmulz  12673  xrsupexmnf  13021  xrinfmexpnf  13022  caubnd2  15050  caurcvg  15369  caurcvg2  15370  caucvg  15371  sgrpidmnd  18371  txlm  22780  norm1exi  29591  chrelat2i  30706  xrofsup  31069  esumcvg  32033  bnj168  32688  satfv1  33304  satfv0fvfmla0  33354  poimirlem30  35786  ismblfin  35797  dffltz  40451  allbutfi  42887  sge0ltfirpmpt  43900  ovolval5lem3  44146  2reu8i  44556  nnsum4primes4  45193  nnsum4primesprm  45195  nnsum4primesgbe  45197  nnsum4primesle9  45199  0aryfvalelfv  45933