Theorem reximdvai 3199

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-rex 3069

This theorem is referenced by:  reximdv  3201  reximdva  3202  reuind  3683  wefrc  5574  isomin  7188  isofrlem  7191  onfununi  8143  oaordex  8351  odi  8372  omass  8373  omeulem1  8375  noinfep  9348  dftrpred3g  9412  rankwflemb  9482  infxpenlem  9700  coflim  9948  coftr  9960  zorn2lem7  10189  suplem1pr  10739  axpre-sup  10856  climbdd  15311  filufint  22979  cvati  30629  atcvat4i  30660  mdsymlem2  30667  mdsymlem3  30668  sumdmdii  30678  iccllysconn  33112  incsequz2  35834  lcvat  36971  hlrelat3  37353  cvrval3  37354  cvrval4N  37355  2atlt  37380  cvrat4  37384  atbtwnexOLDN  37388  atbtwnex  37389  athgt  37397  2llnmat  37465  lnjatN  37721  2lnat  37725  cdlemb  37735  lhpexle3lem  37952  cdlemf1  38502  cdlemf2  38503  cdlemf  38504  cdlemk26b-3  38846  dvh4dimlem  39384  upbdrech  42734  limcperiod  43059  cncfshift  43305  cncfperiod  43310