Theorem reximdvai 3154

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

Syntax hints:   → wi 4   ∈ wcel 2098  ∃wrex 3059

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-rex 3060

This theorem is referenced by:  reximdva  3157  reximdv  3159  reuind  3745  wefrc  5672  isomin  7344  isofrlem  7347  onfununi  8362  oaordex  8579  odi  8600  omass  8601  omeulem1  8603  noinfep  9685  rankwflemb  9818  infxpenlem  10038  coflim  10286  coftr  10298  zorn2lem7  10527  suplem1pr  11077  axpre-sup  11194  climbdd  15654  filufint  23868  cvati  32248  atcvat4i  32279  mdsymlem2  32286  mdsymlem3  32287  sumdmdii  32297  iccllysconn  34991  incsequz2  37353  lcvat  38632  hlrelat3  39015  cvrval3  39016  cvrval4N  39017  2atlt  39042  cvrat4  39046  atbtwnexOLDN  39050  atbtwnex  39051  athgt  39059  2llnmat  39127  lnjatN  39383  2lnat  39387  cdlemb  39397  lhpexle3lem  39614  cdlemf1  40164  cdlemf2  40165  cdlemf  40166  cdlemk26b-3  40508  dvh4dimlem  41046  cantnf2  42896  upbdrech  44825  limcperiod  45154  cncfshift  45400  cncfperiod  45405