Theorem reximdvai 3151

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

Syntax hints:   → wi 4   ∈ wcel 2108  ∃wrex 3060

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 3061

This theorem is referenced by:  reximdva  3153  reximdv  3155  reuind  3736  wefrc  5648  isomin  7330  isofrlem  7333  onfununi  8355  oaordex  8570  odi  8591  omass  8592  omeulem1  8594  noinfep  9674  rankwflemb  9807  infxpenlem  10027  coflim  10275  coftr  10287  zorn2lem7  10516  suplem1pr  11066  axpre-sup  11183  climbdd  15688  filufint  23858  cvati  32347  atcvat4i  32378  mdsymlem2  32385  mdsymlem3  32386  sumdmdii  32396  iccllysconn  35272  incsequz2  37773  lcvat  39048  hlrelat3  39431  cvrval3  39432  cvrval4N  39433  2atlt  39458  cvrat4  39462  atbtwnexOLDN  39466  atbtwnex  39467  athgt  39475  2llnmat  39543  lnjatN  39799  2lnat  39803  cdlemb  39813  lhpexle3lem  40030  cdlemf1  40580  cdlemf2  40581  cdlemf  40582  cdlemk26b-3  40924  dvh4dimlem  41462  cantnf2  43349  relpfrlem  44978  upbdrech  45334  limcperiod  45657  cncfshift  45903  cncfperiod  45908