Theorem reximdvai 3149

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

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

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 3063

This theorem is referenced by:  reximdva  3151  reximdv  3153  reuind  3700  wefrc  5618  isomin  7285  isofrlem  7288  onfununi  8274  oaordex  8486  odi  8507  omass  8508  omeulem1  8510  noinfep  9572  rankwflemb  9708  infxpenlem  9926  coflim  10174  coftr  10186  zorn2lem7  10415  suplem1pr  10966  axpre-sup  11083  climbdd  15625  filufint  23895  cvati  32452  atcvat4i  32483  mdsymlem2  32490  mdsymlem3  32491  sumdmdii  32501  iccllysconn  35448  incsequz2  38084  lcvat  39490  hlrelat3  39872  cvrval3  39873  cvrval4N  39874  2atlt  39899  cvrat4  39903  atbtwnexOLDN  39907  atbtwnex  39908  athgt  39916  2llnmat  39984  lnjatN  40240  2lnat  40244  cdlemb  40254  lhpexle3lem  40471  cdlemf1  41021  cdlemf2  41022  cdlemf  41023  cdlemk26b-3  41365  dvh4dimlem  41903  cantnf2  43771  relpfrlem  45398  upbdrech  45756  limcperiod  46076  cncfshift  46320  cncfperiod  46325  chnsubseqword  47324