Theorem reximdvai 3145

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

Syntax hints:   → wi 4   ∈ wcel 2109  ∃wrex 3054

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3055

This theorem is referenced by:  reximdva  3147  reximdv  3149  reuind  3726  wefrc  5634  isomin  7314  isofrlem  7317  onfununi  8312  oaordex  8524  odi  8545  omass  8546  omeulem1  8548  noinfep  9619  rankwflemb  9752  infxpenlem  9972  coflim  10220  coftr  10232  zorn2lem7  10461  suplem1pr  11011  axpre-sup  11128  climbdd  15644  filufint  23813  cvati  32301  atcvat4i  32332  mdsymlem2  32339  mdsymlem3  32340  sumdmdii  32350  iccllysconn  35237  incsequz2  37738  lcvat  39018  hlrelat3  39401  cvrval3  39402  cvrval4N  39403  2atlt  39428  cvrat4  39432  atbtwnexOLDN  39436  atbtwnex  39437  athgt  39445  2llnmat  39513  lnjatN  39769  2lnat  39773  cdlemb  39783  lhpexle3lem  40000  cdlemf1  40550  cdlemf2  40551  cdlemf  40552  cdlemk26b-3  40894  dvh4dimlem  41432  cantnf2  43307  relpfrlem  44936  upbdrech  45296  limcperiod  45619  cncfshift  45865  cncfperiod  45870