Theorem reximdvai 3200

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 571	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) → (𝑥 ∈ 𝐴 ∧ 𝜒)))
3	2	reximdv2 3199	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ∈ wcel 2106  ∃wrex 3065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-rex 3070

This theorem is referenced by:  reximdv  3202  reximdva  3203  reuind  3688  wefrc  5583  isomin  7208  isofrlem  7211  onfununi  8172  oaordex  8389  odi  8410  omass  8411  omeulem1  8413  noinfep  9418  rankwflemb  9551  infxpenlem  9769  coflim  10017  coftr  10029  zorn2lem7  10258  suplem1pr  10808  axpre-sup  10925  climbdd  15383  filufint  23071  cvati  30728  atcvat4i  30759  mdsymlem2  30766  mdsymlem3  30767  sumdmdii  30777  iccllysconn  33212  incsequz2  35907  lcvat  37044  hlrelat3  37426  cvrval3  37427  cvrval4N  37428  2atlt  37453  cvrat4  37457  atbtwnexOLDN  37461  atbtwnex  37462  athgt  37470  2llnmat  37538  lnjatN  37794  2lnat  37798  cdlemb  37808  lhpexle3lem  38025  cdlemf1  38575  cdlemf2  38576  cdlemf  38577  cdlemk26b-3  38919  dvh4dimlem  39457  upbdrech  42844  limcperiod  43169  cncfshift  43415  cncfperiod  43420