Theorem reximdvai 3165

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

Syntax hints:   → wi 4   ∈ wcel 2106  ∃wrex 3070

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 1913

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-rex 3071

This theorem is referenced by:  reximdva  3168  reximdv  3170  reuind  3749  wefrc  5670  isomin  7336  isofrlem  7339  onfununi  8343  oaordex  8560  odi  8581  omass  8582  omeulem1  8584  noinfep  9657  rankwflemb  9790  infxpenlem  10010  coflim  10258  coftr  10270  zorn2lem7  10499  suplem1pr  11049  axpre-sup  11166  climbdd  15620  filufint  23431  cvati  31657  atcvat4i  31688  mdsymlem2  31695  mdsymlem3  31696  sumdmdii  31706  iccllysconn  34310  incsequz2  36703  lcvat  37986  hlrelat3  38369  cvrval3  38370  cvrval4N  38371  2atlt  38396  cvrat4  38400  atbtwnexOLDN  38404  atbtwnex  38405  athgt  38413  2llnmat  38481  lnjatN  38737  2lnat  38741  cdlemb  38751  lhpexle3lem  38968  cdlemf1  39518  cdlemf2  39519  cdlemf  39520  cdlemk26b-3  39862  dvh4dimlem  40400  cantnf2  42157  upbdrech  44094  limcperiod  44423  cncfshift  44669  cncfperiod  44674