Theorem reximdvai 3144

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

Syntax hints:   → wi 4   ∈ wcel 2109  ∃wrex 3053

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 3054

This theorem is referenced by:  reximdva  3146  reximdv  3148  reuind  3721  wefrc  5625  isomin  7294  isofrlem  7297  onfununi  8287  oaordex  8499  odi  8520  omass  8521  omeulem1  8523  noinfep  9589  rankwflemb  9722  infxpenlem  9942  coflim  10190  coftr  10202  zorn2lem7  10431  suplem1pr  10981  axpre-sup  11098  climbdd  15614  filufint  23783  cvati  32268  atcvat4i  32299  mdsymlem2  32306  mdsymlem3  32307  sumdmdii  32317  iccllysconn  35210  incsequz2  37716  lcvat  38996  hlrelat3  39379  cvrval3  39380  cvrval4N  39381  2atlt  39406  cvrat4  39410  atbtwnexOLDN  39414  atbtwnex  39415  athgt  39423  2llnmat  39491  lnjatN  39747  2lnat  39751  cdlemb  39761  lhpexle3lem  39978  cdlemf1  40528  cdlemf2  40529  cdlemf  40530  cdlemk26b-3  40872  dvh4dimlem  41410  cantnf2  43287  relpfrlem  44916  upbdrech  45276  limcperiod  45599  cncfshift  45845  cncfperiod  45850