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 2145  ∃wrex 3086

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

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

This theorem is used by:  reximdva  3175  reximdv  3177  reuind  3711  wefrc  5649  isomin  7338  isofrlem  7341  onfununi  8330  oaordex  8545  odi  8566  omass  8567  omeulem1  8569  noinfep  9639  rankwflemb  9775  infxpenlem  10016  coflim  10263  coftr  10275  zorn2lem7  10504  suplem1pr  11061  axpre-sup  11178  climbdd  15759  filufint  24146  cvati  32847  atcvat4i  32878  mdsymlem2  32885  mdsymlem3  32886  sumdmdii  32896  iccllysconn  35829  incsequz2  38499  lcvat  39903  hlrelat3  40285  cvrval3  40286  cvrval4N  40287  2atlt  40312  cvrat4  40316  atbtwnexOLDN  40320  atbtwnex  40321  athgt  40329  2llnmat  40397  lnjatN  40653  2lnat  40657  cdlemb  40667  lhpexle3lem  40884  cdlemf1  41434  cdlemf2  41435  cdlemf  41436  cdlemk26b-3  41778  dvh4dimlem  42316  cantnf2  44166  relpfrlem  45776  upbdrech  46138  limcperiod  46458  cncfshift  46702  cncfperiod  46707