Theorem reximdvai 2998

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

Syntax hints:   → wi 4   ∈ wcel 1977  ∀wral 2896  ∃wrex 2897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827

This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-ral 2901  df-rex 2902

This theorem is referenced by:  reximdv  2999  reximdva  3000  reuind  3378  wefrc  5032  isomin  6487  isofrlem  6490  onfununi  7325  oaordex  7525  odi  7546  omass  7547  omeulem1  7549  noinfep  8440  rankwflemb  8539  infxpenlem  8719  coflim  8966  coftr  8978  zorn2lem7  9207  suplem1pr  9753  axpre-sup  9869  climbdd  14250  filufint  21534  cvati  28609  atcvat4i  28640  mdsymlem2  28647  mdsymlem3  28648  sumdmdii  28658  iccllyscon  30486  dftrpred3g  30977  incsequz2  32715  lcvat  33335  hlrelat3  33716  cvrval3  33717  cvrval4N  33718  2atlt  33743  cvrat4  33747  atbtwnexOLDN  33751  atbtwnex  33752  athgt  33760  2llnmat  33828  lnjatN  34084  2lnat  34088  cdlemb  34098  lhpexle3lem  34315  cdlemf1  34867  cdlemf2  34868  cdlemf  34869  cdlemk26b-3  35211  dvh4dimlem  35750  upbdrech  38460  limcperiod  38695  cncfshift  38759  cncfperiod  38764