Theorem reximia 3072

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 568	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → (𝑥 ∈ 𝐴 ∧ 𝜓))
3	2	reximi2 3070	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ∈ wcel 2114  ∃wrex 3061

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-rex 3062

This theorem is referenced by:  reximi  3075  iunpw  7725  tz7.49c  8385  fisup2g  9382  fiinf2g  9415  unwdomg  9499  trcl  9649  cfsmolem  10192  1idpr  10952  qmulz  12901  xrsupexmnf  13257  xrinfmexpnf  13258  caubnd2  15320  caurcvg  15639  caurcvg2  15640  caucvg  15641  sgrpidmnd  18707  txlm  23613  znegscl  28384  z12negscl  28470  norm1exi  31321  chrelat2i  32436  xrofsup  32840  esumcvg  34230  bnj168  34873  satfv1  35545  satfv0fvfmla0  35595  poimirlem30  37971  ismblfin  37982  dffltz  43067  allbutfi  45822  sge0ltfirpmpt  46836  ovolval5lem3  47082  2reu8i  47561  nnsum4primes4  48265  nnsum4primesprm  48267  nnsum4primesgbe  48269  nnsum4primesle9  48271  0aryfvalelfv  49111