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 2109  ∃wrex 3053

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 3054

This theorem is referenced by:  reximdva  3146  reximdv  3148  reuind  3724  wefrc  5632  isomin  7312  isofrlem  7315  onfununi  8310  oaordex  8522  odi  8543  omass  8544  omeulem1  8546  noinfep  9613  rankwflemb  9746  infxpenlem  9966  coflim  10214  coftr  10226  zorn2lem7  10455  suplem1pr  11005  axpre-sup  11122  climbdd  15638  filufint  23807  cvati  32295  atcvat4i  32326  mdsymlem2  32333  mdsymlem3  32334  sumdmdii  32344  iccllysconn  35237  incsequz2  37743  lcvat  39023  hlrelat3  39406  cvrval3  39407  cvrval4N  39408  2atlt  39433  cvrat4  39437  atbtwnexOLDN  39441  atbtwnex  39442  athgt  39450  2llnmat  39518  lnjatN  39774  2lnat  39778  cdlemb  39788  lhpexle3lem  40005  cdlemf1  40555  cdlemf2  40556  cdlemf  40557  cdlemk26b-3  40899  dvh4dimlem  41437  cantnf2  43314  relpfrlem  44943  upbdrech  45303  limcperiod  45626  cncfshift  45872  cncfperiod  45877