Theorem reximdvai 3158

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

Syntax hints:   → wi 4   ∈ wcel 2106  ∃wrex 3069

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 1913

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-rex 3070

This theorem is referenced by:  reximdva  3161  reximdv  3163  reuind  3714  wefrc  5632  isomin  7287  isofrlem  7290  onfununi  8292  oaordex  8510  odi  8531  omass  8532  omeulem1  8534  noinfep  9605  rankwflemb  9738  infxpenlem  9958  coflim  10206  coftr  10218  zorn2lem7  10447  suplem1pr  10997  axpre-sup  11114  climbdd  15568  filufint  23308  cvati  31371  atcvat4i  31402  mdsymlem2  31409  mdsymlem3  31410  sumdmdii  31420  iccllysconn  33931  incsequz2  36281  lcvat  37565  hlrelat3  37948  cvrval3  37949  cvrval4N  37950  2atlt  37975  cvrat4  37979  atbtwnexOLDN  37983  atbtwnex  37984  athgt  37992  2llnmat  38060  lnjatN  38316  2lnat  38320  cdlemb  38330  lhpexle3lem  38547  cdlemf1  39097  cdlemf2  39098  cdlemf  39099  cdlemk26b-3  39441  dvh4dimlem  39979  cantnf2  41718  upbdrech  43660  limcperiod  43989  cncfshift  44235  cncfperiod  44240