Theorem reximdvai 3144

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

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

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 3058

This theorem is referenced by:  reximdva  3146  reximdv  3148  reuind  3708  wefrc  5615  isomin  7280  isofrlem  7283  onfununi  8270  oaordex  8482  odi  8503  omass  8504  omeulem1  8506  noinfep  9561  rankwflemb  9697  infxpenlem  9915  coflim  10163  coftr  10175  zorn2lem7  10404  suplem1pr  10954  axpre-sup  11071  climbdd  15586  filufint  23855  cvati  32367  atcvat4i  32398  mdsymlem2  32405  mdsymlem3  32406  sumdmdii  32416  iccllysconn  35366  incsequz2  37862  lcvat  39202  hlrelat3  39584  cvrval3  39585  cvrval4N  39586  2atlt  39611  cvrat4  39615  atbtwnexOLDN  39619  atbtwnex  39620  athgt  39628  2llnmat  39696  lnjatN  39952  2lnat  39956  cdlemb  39966  lhpexle3lem  40183  cdlemf1  40733  cdlemf2  40734  cdlemf  40735  cdlemk26b-3  41077  dvh4dimlem  41615  cantnf2  43482  relpfrlem  45110  upbdrech  45469  limcperiod  45790  cncfshift  46034  cncfperiod  46039  chnsubseqword  47038