Theorem reximdvai 3148

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

Syntax hints:   → wi 4   ∈ wcel 2114  ∃wrex 3061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-rex 3062

This theorem is referenced by:  reximdva  3150  reximdv  3152  reuind  3699  wefrc  5625  isomin  7292  isofrlem  7295  onfununi  8281  oaordex  8493  odi  8514  omass  8515  omeulem1  8517  noinfep  9581  rankwflemb  9717  infxpenlem  9935  coflim  10183  coftr  10195  zorn2lem7  10424  suplem1pr  10975  axpre-sup  11092  climbdd  15634  filufint  23885  cvati  32437  atcvat4i  32468  mdsymlem2  32475  mdsymlem3  32476  sumdmdii  32486  iccllysconn  35432  incsequz2  38070  lcvat  39476  hlrelat3  39858  cvrval3  39859  cvrval4N  39860  2atlt  39885  cvrat4  39889  atbtwnexOLDN  39893  atbtwnex  39894  athgt  39902  2llnmat  39970  lnjatN  40226  2lnat  40230  cdlemb  40240  lhpexle3lem  40457  cdlemf1  41007  cdlemf2  41008  cdlemf  41009  cdlemk26b-3  41351  dvh4dimlem  41889  cantnf2  43753  relpfrlem  45380  upbdrech  45738  limcperiod  46058  cncfshift  46302  cncfperiod  46307  chnsubseqword  47308