Theorem reximdvai 3178

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  ∃wrex 3091

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 3092

This theorem is used by:  reximdva  3180  reximdv  3182  reuind  3718  wefrc  5657  isomin  7344  isofrlem  7347  onfununi  8334  oaordex  8549  odi  8570  omass  8571  omeulem1  8573  noinfep  9636  rankwflemb  9772  infxpenlem  10013  coflim  10260  coftr  10272  zorn2lem7  10501  suplem1pr  11052  axpre-sup  11169  climbdd  15747  filufint  24128  cvati  32789  atcvat4i  32820  mdsymlem2  32827  mdsymlem3  32828  sumdmdii  32838  iccllysconn  35779  incsequz2  38458  lcvat  39862  hlrelat3  40244  cvrval3  40245  cvrval4N  40246  2atlt  40271  cvrat4  40275  atbtwnexOLDN  40279  atbtwnex  40280  athgt  40288  2llnmat  40356  lnjatN  40612  2lnat  40616  cdlemb  40626  lhpexle3lem  40843  cdlemf1  41393  cdlemf2  41394  cdlemf  41395  cdlemk26b-3  41737  dvh4dimlem  42275  cantnf2  44110  relpfrlem  45720  upbdrech  46082  limcperiod  46402  cncfshift  46646  cncfperiod  46651  chnsubseqword  47652