Theorem reximdvai 3140

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 3139	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  3142  reximdv  3144  reuind  3715  wefrc  5617  isomin  7278  isofrlem  7281  onfununi  8271  oaordex  8483  odi  8504  omass  8505  omeulem1  8507  noinfep  9575  rankwflemb  9708  infxpenlem  9926  coflim  10174  coftr  10186  zorn2lem7  10415  suplem1pr  10965  axpre-sup  11082  climbdd  15598  filufint  23824  cvati  32329  atcvat4i  32360  mdsymlem2  32367  mdsymlem3  32368  sumdmdii  32378  iccllysconn  35242  incsequz2  37748  lcvat  39028  hlrelat3  39411  cvrval3  39412  cvrval4N  39413  2atlt  39438  cvrat4  39442  atbtwnexOLDN  39446  atbtwnex  39447  athgt  39455  2llnmat  39523  lnjatN  39779  2lnat  39783  cdlemb  39793  lhpexle3lem  40010  cdlemf1  40560  cdlemf2  40561  cdlemf  40562  cdlemk26b-3  40904  dvh4dimlem  41442  cantnf2  43318  relpfrlem  44947  upbdrech  45307  limcperiod  45629  cncfshift  45875  cncfperiod  45880