Theorem reximdvai 3202

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

Syntax hints:   → wi 4   ∈ wcel 2110  ∃wrex 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1787  df-rex 3072

This theorem is referenced by:  reximdv  3204  reximdva  3205  reuind  3692  wefrc  5584  isomin  7204  isofrlem  7207  onfununi  8163  oaordex  8374  odi  8395  omass  8396  omeulem1  8398  noinfep  9396  dftrpred3g  9481  rankwflemb  9552  infxpenlem  9770  coflim  10018  coftr  10030  zorn2lem7  10259  suplem1pr  10809  axpre-sup  10926  climbdd  15381  filufint  23069  cvati  30724  atcvat4i  30755  mdsymlem2  30762  mdsymlem3  30763  sumdmdii  30773  iccllysconn  33208  incsequz2  35903  lcvat  37040  hlrelat3  37422  cvrval3  37423  cvrval4N  37424  2atlt  37449  cvrat4  37453  atbtwnexOLDN  37457  atbtwnex  37458  athgt  37466  2llnmat  37534  lnjatN  37790  2lnat  37794  cdlemb  37804  lhpexle3lem  38021  cdlemf1  38571  cdlemf2  38572  cdlemf  38573  cdlemk26b-3  38915  dvh4dimlem  39453  upbdrech  42815  limcperiod  43140  cncfshift  43386  cncfperiod  43391