Theorem reximdvai 3173

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

Syntax hints:   → wi 4   ∈ wcel 2142  ∃wrex 3086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-rex 3087

This theorem is referenced by:  reximdva  3175  reximdv  3177  reuind  3716  wefrc  5641  isomin  7321  isofrlem  7324  onfununi  8312  oaordex  8527  odi  8548  omass  8549  omeulem1  8551  noinfep  9615  rankwflemb  9751  infxpenlem  9969  coflim  10218  coftr  10230  zorn2lem7  10459  suplem1pr  11010  axpre-sup  11127  climbdd  15699  filufint  23977  cvati  32566  atcvat4i  32597  mdsymlem2  32604  mdsymlem3  32605  sumdmdii  32615  iccllysconn  35597  incsequz2  38245  lcvat  39651  hlrelat3  40033  cvrval3  40034  cvrval4N  40035  2atlt  40060  cvrat4  40064  atbtwnexOLDN  40068  atbtwnex  40069  athgt  40077  2llnmat  40145  lnjatN  40401  2lnat  40405  cdlemb  40415  lhpexle3lem  40632  cdlemf1  41182  cdlemf2  41183  cdlemf  41184  cdlemk26b-3  41526  dvh4dimlem  42064  cantnf2  43899  relpfrlem  45526  upbdrech  45881  limcperiod  46201  cncfshift  46445  cncfperiod  46450  chnsubseqword  47451