Theorem reximdvai 3174

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ∃wrex 3087

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 3088

This theorem is used by:  reximdva  3176  reximdv  3178  reuind  3711  wefrc  5645  isomin  7343  isofrlem  7346  onfununi  8342  oaordex  8559  odi  8580  omass  8581  omeulem1  8583  noinfep  9654  rankwflemb  9793  rankwflembOLD  9794  infxpenlem  10085  coflim  10332  coftr  10344  zorn2lem7  10573  suplem1pr  11130  axpre-sup  11247  climbdd  15832  filufint  24232  cvati  32961  atcvat4i  32992  mdsymlem2  32999  mdsymlem3  33000  sumdmdii  33010  iccllysconn  35994  incsequz2  38663  lcvat  40067  hlrelat3  40449  cvrval3  40450  cvrval4N  40451  2atlt  40476  cvrat4  40480  atbtwnexOLDN  40484  atbtwnex  40485  athgt  40493  2llnmat  40561  lnjatN  40817  2lnat  40821  cdlemb  40831  lhpexle3lem  41048  cdlemf1  41598  cdlemf2  41599  cdlemf  41600  cdlemk26b-3  41942  dvh4dimlem  42480  cantnf2  44311  relpfrlem  45921  upbdrech  46290  limcperiod  46609  cncfshift  46853  cncfperiod  46858