Theorem reximdvai 3177

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  ∃wrex 3090

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-rex 3091

This theorem is used by:  reximdva  3179  reximdv  3181  reuind  3714  wefrc  5652  isomin  7376  isofrlem  7379  onfununi  8387  oaordex  8604  odi  8625  omass  8626  omeulem1  8628  noinfep  9698  rankwflemb  9837  rankwflembOLD  9838  infxpenlem  10131  coflim  10378  coftr  10390  zorn2lem7  10619  suplem1pr  11176  axpre-sup  11293  climbdd  15883  filufint  24294  cvati  33025  atcvat4i  33056  mdsymlem2  33063  mdsymlem3  33064  sumdmdii  33074  iccllysconn  36223  incsequz2  38949  lcvat  40353  hlrelat3  40735  cvrval3  40736  cvrval4N  40737  2atlt  40762  cvrat4  40766  atbtwnexOLDN  40770  atbtwnex  40771  athgt  40779  2llnmat  40847  lnjatN  41103  2lnat  41107  cdlemb  41117  lhpexle3lem  41334  cdlemf1  41884  cdlemf2  41885  cdlemf  41886  cdlemk26b-3  42228  dvh4dimlem  42766  cantnf2  44588  relpfrlem  46207  upbdrech  46594  limcperiod  46913  cncfshift  47157  cncfperiod  47162