Theorem reximia 3064

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 3062	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓)

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

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 207  df-an 396  df-ex 1780  df-rex 3054

This theorem is referenced by:  reximi  3067  iunpw  7747  tz7.49c  8414  fisup2g  9420  fiinf2g  9453  unwdomg  9537  trcl  9681  cfsmolem  10223  1idpr  10982  qmulz  12910  xrsupexmnf  13265  xrinfmexpnf  13266  caubnd2  15324  caurcvg  15643  caurcvg2  15644  caucvg  15645  sgrpidmnd  18666  txlm  23535  znegscl  28280  zs12negscl  28340  norm1exi  31179  chrelat2i  32294  xrofsup  32690  esumcvg  34076  bnj168  34720  satfv1  35350  satfv0fvfmla0  35400  poimirlem30  37644  ismblfin  37655  dffltz  42622  allbutfi  45389  sge0ltfirpmpt  46406  ovolval5lem3  46652  2reu8i  47114  nnsum4primes4  47790  nnsum4primesprm  47792  nnsum4primesgbe  47794  nnsum4primesle9  47796  0aryfvalelfv  48624