Theorem reximdvai 3164

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

Syntax hints:   → wi 4   ∈ wcel 2105  ∃wrex 3069

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1781  df-rex 3070

This theorem is referenced by:  reximdva  3167  reximdv  3169  reuind  3749  wefrc  5670  isomin  7337  isofrlem  7340  onfununi  8345  oaordex  8562  odi  8583  omass  8584  omeulem1  8586  noinfep  9659  rankwflemb  9792  infxpenlem  10012  coflim  10260  coftr  10272  zorn2lem7  10501  suplem1pr  11051  axpre-sup  11168  climbdd  15623  filufint  23645  cvati  31887  atcvat4i  31918  mdsymlem2  31925  mdsymlem3  31926  sumdmdii  31936  iccllysconn  34540  incsequz2  36921  lcvat  38204  hlrelat3  38587  cvrval3  38588  cvrval4N  38589  2atlt  38614  cvrat4  38618  atbtwnexOLDN  38622  atbtwnex  38623  athgt  38631  2llnmat  38699  lnjatN  38955  2lnat  38959  cdlemb  38969  lhpexle3lem  39186  cdlemf1  39736  cdlemf2  39737  cdlemf  39738  cdlemk26b-3  40080  dvh4dimlem  40618  cantnf2  42378  upbdrech  44314  limcperiod  44643  cncfshift  44889  cncfperiod  44894