Theorem reximdvai 3165

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

Syntax hints:   → wi 4   ∈ wcel 2108  ∃wrex 3070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3071

This theorem is referenced by:  reximdva  3168  reximdv  3170  reuind  3759  wefrc  5679  isomin  7357  isofrlem  7360  onfununi  8381  oaordex  8596  odi  8617  omass  8618  omeulem1  8620  noinfep  9700  rankwflemb  9833  infxpenlem  10053  coflim  10301  coftr  10313  zorn2lem7  10542  suplem1pr  11092  axpre-sup  11209  climbdd  15708  filufint  23928  cvati  32385  atcvat4i  32416  mdsymlem2  32423  mdsymlem3  32424  sumdmdii  32434  iccllysconn  35255  incsequz2  37756  lcvat  39031  hlrelat3  39414  cvrval3  39415  cvrval4N  39416  2atlt  39441  cvrat4  39445  atbtwnexOLDN  39449  atbtwnex  39450  athgt  39458  2llnmat  39526  lnjatN  39782  2lnat  39786  cdlemb  39796  lhpexle3lem  40013  cdlemf1  40563  cdlemf2  40564  cdlemf  40565  cdlemk26b-3  40907  dvh4dimlem  41445  cantnf2  43338  relpfrlem  44974  upbdrech  45317  limcperiod  45643  cncfshift  45889  cncfperiod  45894