Theorem reximdvai 3272

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.)

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	ralrimiv 3181	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝜓 → 𝜒))
3		rexim 3241	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜓 → 𝜒) → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒))
4	2, 3	syl 17	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ∈ wcel 2110  ∀wral 3138  ∃wrex 3139

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 1907

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-ral 3143  df-rex 3144

This theorem is referenced by:  reximdv  3273  reximdva  3274  reuind  3744  wefrc  5544  isomin  7084  isofrlem  7087  onfununi  7972  oaordex  8178  odi  8199  omass  8200  omeulem1  8202  noinfep  9117  rankwflemb  9216  infxpenlem  9433  coflim  9677  coftr  9689  zorn2lem7  9918  suplem1pr  10468  axpre-sup  10585  climbdd  15022  filufint  22522  cvati  30137  atcvat4i  30168  mdsymlem2  30175  mdsymlem3  30176  sumdmdii  30186  iccllysconn  32492  dftrpred3g  33067  incsequz2  35018  lcvat  36160  hlrelat3  36542  cvrval3  36543  cvrval4N  36544  2atlt  36569  cvrat4  36573  atbtwnexOLDN  36577  atbtwnex  36578  athgt  36586  2llnmat  36654  lnjatN  36910  2lnat  36914  cdlemb  36924  lhpexle3lem  37141  cdlemf1  37691  cdlemf2  37692  cdlemf  37693  cdlemk26b-3  38035  dvh4dimlem  38573  upbdrech  41564  limcperiod  41901  cncfshift  42149  cncfperiod  42154