Theorem reximdvai 3274

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

Syntax hints:   → wi 4   ∈ wcel 2114  ∀wral 3140  ∃wrex 3141

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-ral 3145  df-rex 3146

This theorem is referenced by:  reximdv  3275  reximdva  3276  reuind  3746  wefrc  5551  isomin  7092  isofrlem  7095  onfununi  7980  oaordex  8186  odi  8207  omass  8208  omeulem1  8210  noinfep  9125  rankwflemb  9224  infxpenlem  9441  coflim  9685  coftr  9697  zorn2lem7  9926  suplem1pr  10476  axpre-sup  10593  climbdd  15030  filufint  22530  cvati  30145  atcvat4i  30176  mdsymlem2  30183  mdsymlem3  30184  sumdmdii  30194  iccllysconn  32499  dftrpred3g  33074  incsequz2  35026  lcvat  36168  hlrelat3  36550  cvrval3  36551  cvrval4N  36552  2atlt  36577  cvrat4  36581  atbtwnexOLDN  36585  atbtwnex  36586  athgt  36594  2llnmat  36662  lnjatN  36918  2lnat  36922  cdlemb  36932  lhpexle3lem  37149  cdlemf1  37699  cdlemf2  37700  cdlemf  37701  cdlemk26b-3  38043  dvh4dimlem  38581  upbdrech  41579  limcperiod  41916  cncfshift  42164  cncfperiod  42169