Theorem reximdvai 3176

Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 14-Nov-2002.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 8-Jan-2020.) (Proof shortened by Wolf Lammen, 4-Nov-2024.)

Hypothesis

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

Assertion

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

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem reximdvai

Step	Hyp	Ref	Expression
1		reximdvai.1	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))
2	1	imdistand 580	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) → (𝑥 ∈ 𝐴 ∧ 𝜒)))
3	2	reximdv2 3175	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ∈ wcel 2143  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-rex 3090

This theorem is referenced by:  reximdva  3178  reximdv  3180  reuind  3716  wefrc  5655  isomin  7335  isofrlem  7338  onfununi  8324  oaordex  8539  odi  8560  omass  8561  omeulem1  8563  noinfep  9625  rankwflemb  9761  infxpenlem  9993  coflim  10240  coftr  10252  zorn2lem7  10481  suplem1pr  11032  axpre-sup  11149  climbdd  15719  filufint  24077  cvati  32718  atcvat4i  32749  mdsymlem2  32756  mdsymlem3  32757  sumdmdii  32767  iccllysconn  35742  incsequz2  38400  lcvat  39804  hlrelat3  40186  cvrval3  40187  cvrval4N  40188  2atlt  40213  cvrat4  40217  atbtwnexOLDN  40221  atbtwnex  40222  athgt  40230  2llnmat  40298  lnjatN  40554  2lnat  40558  cdlemb  40568  lhpexle3lem  40785  cdlemf1  41335  cdlemf2  41336  cdlemf  41337  cdlemk26b-3  41679  dvh4dimlem  42217  cantnf2  44052  relpfrlem  45662  upbdrech  46024  limcperiod  46344  cncfshift  46588  cncfperiod  46593  chnsubseqword  47594