Theorem reximdvai 3147

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

Syntax hints:   → wi 4   ∈ wcel 2113  ∃wrex 3060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-rex 3061

This theorem is referenced by:  reximdva  3149  reximdv  3151  reuind  3711  wefrc  5618  isomin  7283  isofrlem  7286  onfununi  8273  oaordex  8485  odi  8506  omass  8507  omeulem1  8509  noinfep  9569  rankwflemb  9705  infxpenlem  9923  coflim  10171  coftr  10183  zorn2lem7  10412  suplem1pr  10963  axpre-sup  11080  climbdd  15595  filufint  23864  cvati  32441  atcvat4i  32472  mdsymlem2  32479  mdsymlem3  32480  sumdmdii  32490  iccllysconn  35444  incsequz2  37950  lcvat  39290  hlrelat3  39672  cvrval3  39673  cvrval4N  39674  2atlt  39699  cvrat4  39703  atbtwnexOLDN  39707  atbtwnex  39708  athgt  39716  2llnmat  39784  lnjatN  40040  2lnat  40044  cdlemb  40054  lhpexle3lem  40271  cdlemf1  40821  cdlemf2  40822  cdlemf  40823  cdlemk26b-3  41165  dvh4dimlem  41703  cantnf2  43567  relpfrlem  45194  upbdrech  45553  limcperiod  45874  cncfshift  46118  cncfperiod  46123  chnsubseqword  47122