Theorem reximdvai 3161

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

Syntax hints:   → wi 4   ∈ wcel 2155  ∀wral 3055  ∃wrex 3056

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005

This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1875  df-ral 3060  df-rex 3061

This theorem is referenced by:  reximdv  3162  reximdva  3163  reuind  3572  wefrc  5271  isomin  6779  isofrlem  6782  onfununi  7642  oaordex  7843  odi  7864  omass  7865  omeulem1  7867  noinfep  8772  rankwflemb  8871  infxpenlem  9087  coflim  9336  coftr  9348  zorn2lem7  9577  suplem1pr  10127  axpre-sup  10243  climbdd  14687  filufint  22003  cvati  29681  atcvat4i  29712  mdsymlem2  29719  mdsymlem3  29720  sumdmdii  29730  iccllysconn  31680  dftrpred3g  32176  incsequz2  33967  lcvat  34986  hlrelat3  35368  cvrval3  35369  cvrval4N  35370  2atlt  35395  cvrat4  35399  atbtwnexOLDN  35403  atbtwnex  35404  athgt  35412  2llnmat  35480  lnjatN  35736  2lnat  35740  cdlemb  35750  lhpexle3lem  35967  cdlemf1  36517  cdlemf2  36518  cdlemf  36519  cdlemk26b-3  36861  dvh4dimlem  37399  upbdrech  40158  limcperiod  40498  cncfshift  40725  cncfperiod  40730