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  3727  wefrc  5635  isomin  7315  isofrlem  7318  onfununi  8313  oaordex  8525  odi  8546  omass  8547  omeulem1  8549  noinfep  9620  rankwflemb  9753  infxpenlem  9973  coflim  10221  coftr  10233  zorn2lem7  10462  suplem1pr  11012  axpre-sup  11129  climbdd  15645  filufint  23814  cvati  32302  atcvat4i  32333  mdsymlem2  32340  mdsymlem3  32341  sumdmdii  32351  iccllysconn  35244  incsequz2  37750  lcvat  39030  hlrelat3  39413  cvrval3  39414  cvrval4N  39415  2atlt  39440  cvrat4  39444  atbtwnexOLDN  39448  atbtwnex  39449  athgt  39457  2llnmat  39525  lnjatN  39781  2lnat  39785  cdlemb  39795  lhpexle3lem  40012  cdlemf1  40562  cdlemf2  40563  cdlemf  40564  cdlemk26b-3  40906  dvh4dimlem  41444  cantnf2  43321  relpfrlem  44950  upbdrech  45310  limcperiod  45633  cncfshift  45879  cncfperiod  45884