Theorem reximdvai 3173

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  ∃wrex 3086

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-rex 3087

This theorem is used by:  reximdva  3175  reximdv  3177  reuind  3710  wefrc  5645  isomin  7349  isofrlem  7352  onfununi  8356  oaordex  8573  odi  8594  omass  8595  omeulem1  8597  noinfep  9668  rankwflemb  9807  rankwflembOLD  9808  infxpenlem  10099  coflim  10346  coftr  10358  zorn2lem7  10587  suplem1pr  11144  axpre-sup  11261  climbdd  15848  filufint  24248  cvati  32977  atcvat4i  33008  mdsymlem2  33015  mdsymlem3  33016  sumdmdii  33026  iccllysconn  36105  incsequz2  38792  lcvat  40196  hlrelat3  40578  cvrval3  40579  cvrval4N  40580  2atlt  40605  cvrat4  40609  atbtwnexOLDN  40613  atbtwnex  40614  athgt  40622  2llnmat  40690  lnjatN  40946  2lnat  40950  cdlemb  40960  lhpexle3lem  41177  cdlemf1  41727  cdlemf2  41728  cdlemf  41729  cdlemk26b-3  42071  dvh4dimlem  42609  cantnf2  44436  relpfrlem  46051  upbdrech  46429  limcperiod  46748  cncfshift  46992  cncfperiod  46997