Theorem reximdvai 3163

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

Syntax hints:   → wi 4   ∈ wcel 2106  ∃wrex 3068

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-rex 3069

This theorem is referenced by:  reximdva  3166  reximdv  3168  reuind  3762  wefrc  5683  isomin  7357  isofrlem  7360  onfununi  8380  oaordex  8595  odi  8616  omass  8617  omeulem1  8619  noinfep  9698  rankwflemb  9831  infxpenlem  10051  coflim  10299  coftr  10311  zorn2lem7  10540  suplem1pr  11090  axpre-sup  11207  climbdd  15705  filufint  23944  cvati  32395  atcvat4i  32426  mdsymlem2  32433  mdsymlem3  32434  sumdmdii  32444  iccllysconn  35235  incsequz2  37736  lcvat  39012  hlrelat3  39395  cvrval3  39396  cvrval4N  39397  2atlt  39422  cvrat4  39426  atbtwnexOLDN  39430  atbtwnex  39431  athgt  39439  2llnmat  39507  lnjatN  39763  2lnat  39767  cdlemb  39777  lhpexle3lem  39994  cdlemf1  40544  cdlemf2  40545  cdlemf  40546  cdlemk26b-3  40888  dvh4dimlem  41426  cantnf2  43315  upbdrech  45256  limcperiod  45584  cncfshift  45830  cncfperiod  45835