Theorem reximdvai 3182

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

Syntax hints:   → wi 4   ∈ wcel 2149  ∃wrex 3095

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-rex 3096

This theorem is referenced by:  reximdva  3184  reximdv  3186  reuind  3725  wefrc  5656  isomin  7336  isofrlem  7339  onfununi  8327  oaordex  8542  odi  8563  omass  8564  omeulem1  8566  noinfep  9628  rankwflemb  9764  infxpenlem  9996  coflim  10244  coftr  10256  zorn2lem7  10485  suplem1pr  11036  axpre-sup  11153  climbdd  15722  filufint  24045  cvati  32658  atcvat4i  32689  mdsymlem2  32696  mdsymlem3  32697  sumdmdii  32707  iccllysconn  35640  incsequz2  38287  lcvat  39693  hlrelat3  40075  cvrval3  40076  cvrval4N  40077  2atlt  40102  cvrat4  40106  atbtwnexOLDN  40110  atbtwnex  40111  athgt  40119  2llnmat  40187  lnjatN  40443  2lnat  40447  cdlemb  40457  lhpexle3lem  40674  cdlemf1  41224  cdlemf2  41225  cdlemf  41226  cdlemk26b-3  41568  dvh4dimlem  42106  cantnf2  43943  relpfrlem  45553  upbdrech  45915  limcperiod  46235  cncfshift  46479  cncfperiod  46484  chnsubseqword  47485