Theorem reximia 3081

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

Hypothesis

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

Assertion

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

Proof of Theorem reximia

Step	Hyp	Ref	Expression
1		ralimia.1	. . 3 ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))
2	1	imdistani 570	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → (𝑥 ∈ 𝐴 ∧ 𝜓))
3	2	reximi2 3079	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ∈ wcel 2104  ∃wrex 3071

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

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1780  df-rex 3072

This theorem is referenced by:  reximi  3084  iunpw  7653  wfrdmclOLD  8179  tz7.49c  8308  fisup2g  9271  fiinf2g  9303  unwdomg  9387  trcl  9530  cfsmolem  10072  1idpr  10831  qmulz  12737  xrsupexmnf  13085  xrinfmexpnf  13086  caubnd2  15114  caurcvg  15433  caurcvg2  15434  caucvg  15435  sgrpidmnd  18435  txlm  22844  norm1exi  29657  chrelat2i  30772  xrofsup  31135  esumcvg  32099  bnj168  32754  satfv1  33370  satfv0fvfmla0  33420  poimirlem30  35851  ismblfin  35862  dffltz  40508  allbutfi  42981  sge0ltfirpmpt  43996  ovolval5lem3  44242  2reu8i  44663  nnsum4primes4  45299  nnsum4primesprm  45301  nnsum4primesgbe  45303  nnsum4primesle9  45305  0aryfvalelfv  46039