Theorem reximdvai 3171

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-rex 3077

This theorem is referenced by:  reximdva  3174  reximdv  3176  reuind  3775  wefrc  5694  isomin  7373  isofrlem  7376  onfununi  8397  oaordex  8614  odi  8635  omass  8636  omeulem1  8638  noinfep  9729  rankwflemb  9862  infxpenlem  10082  coflim  10330  coftr  10342  zorn2lem7  10571  suplem1pr  11121  axpre-sup  11238  climbdd  15720  filufint  23949  cvati  32398  atcvat4i  32429  mdsymlem2  32436  mdsymlem3  32437  sumdmdii  32447  iccllysconn  35218  incsequz2  37709  lcvat  38986  hlrelat3  39369  cvrval3  39370  cvrval4N  39371  2atlt  39396  cvrat4  39400  atbtwnexOLDN  39404  atbtwnex  39405  athgt  39413  2llnmat  39481  lnjatN  39737  2lnat  39741  cdlemb  39751  lhpexle3lem  39968  cdlemf1  40518  cdlemf2  40519  cdlemf  40520  cdlemk26b-3  40862  dvh4dimlem  41400  cantnf2  43287  upbdrech  45220  limcperiod  45549  cncfshift  45795  cncfperiod  45800