Theorem reximdvai 3150

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

Syntax hints:   → wi 4   ∈ wcel 2119  ∃wrex 3063

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 208  df-an 397  df-ex 1787  df-rex 3064

This theorem is referenced by:  reximdva  3152  reximdv  3154  reuind  3694  wefrc  5612  isomin  7281  isofrlem  7284  onfununi  8271  oaordex  8483  odi  8504  omass  8505  omeulem1  8507  noinfep  9572  rankwflemb  9708  infxpenlem  9926  coflim  10174  coftr  10186  zorn2lem7  10415  suplem1pr  10966  axpre-sup  11083  climbdd  15625  filufint  23903  cvati  32455  atcvat4i  32486  mdsymlem2  32493  mdsymlem3  32494  sumdmdii  32504  iccllysconn  35478  incsequz2  38116  lcvat  39522  hlrelat3  39904  cvrval3  39905  cvrval4N  39906  2atlt  39931  cvrat4  39935  atbtwnexOLDN  39939  atbtwnex  39940  athgt  39948  2llnmat  40016  lnjatN  40272  2lnat  40276  cdlemb  40286  lhpexle3lem  40503  cdlemf1  41053  cdlemf2  41054  cdlemf  41055  cdlemk26b-3  41397  dvh4dimlem  41935  cantnf2  43770  relpfrlem  45397  upbdrech  45753  limcperiod  46073  cncfshift  46317  cncfperiod  46322  chnsubseqword  47323