Theorem reximdvai 3143

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

Syntax hints:   → wi 4   ∈ wcel 2111  ∃wrex 3056

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 1911

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-rex 3057

This theorem is referenced by:  reximdva  3145  reximdv  3147  reuind  3707  wefrc  5605  isomin  7266  isofrlem  7269  onfununi  8256  oaordex  8468  odi  8489  omass  8490  omeulem1  8492  noinfep  9545  rankwflemb  9681  infxpenlem  9899  coflim  10147  coftr  10159  zorn2lem7  10388  suplem1pr  10938  axpre-sup  11055  climbdd  15574  filufint  23830  cvati  32338  atcvat4i  32369  mdsymlem2  32376  mdsymlem3  32377  sumdmdii  32387  iccllysconn  35286  incsequz2  37789  lcvat  39069  hlrelat3  39451  cvrval3  39452  cvrval4N  39453  2atlt  39478  cvrat4  39482  atbtwnexOLDN  39486  atbtwnex  39487  athgt  39495  2llnmat  39563  lnjatN  39819  2lnat  39823  cdlemb  39833  lhpexle3lem  40050  cdlemf1  40600  cdlemf2  40601  cdlemf  40602  cdlemk26b-3  40944  dvh4dimlem  41482  cantnf2  43358  relpfrlem  44986  upbdrech  45346  limcperiod  45668  cncfshift  45912  cncfperiod  45917