Theorem reximdvai 3149

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

Syntax hints:   → wi 4   ∈ wcel 2114  ∃wrex 3062

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 1912

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-rex 3063

This theorem is referenced by:  reximdva  3151  reximdv  3153  reuind  3713  wefrc  5626  isomin  7293  isofrlem  7296  onfununi  8283  oaordex  8495  odi  8516  omass  8517  omeulem1  8519  noinfep  9581  rankwflemb  9717  infxpenlem  9935  coflim  10183  coftr  10195  zorn2lem7  10424  suplem1pr  10975  axpre-sup  11092  climbdd  15607  filufint  23876  cvati  32454  atcvat4i  32485  mdsymlem2  32492  mdsymlem3  32493  sumdmdii  32503  iccllysconn  35466  incsequz2  38000  lcvat  39406  hlrelat3  39788  cvrval3  39789  cvrval4N  39790  2atlt  39815  cvrat4  39819  atbtwnexOLDN  39823  atbtwnex  39824  athgt  39832  2llnmat  39900  lnjatN  40156  2lnat  40160  cdlemb  40170  lhpexle3lem  40387  cdlemf1  40937  cdlemf2  40938  cdlemf  40939  cdlemk26b-3  41281  dvh4dimlem  41819  cantnf2  43682  relpfrlem  45309  upbdrech  45667  limcperiod  45988  cncfshift  46232  cncfperiod  46237  chnsubseqword  47236