Theorem reximdvai 3232

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

Syntax hints:   → wi 4   ∈ wcel 2079  ∀wral 3103  ∃wrex 3104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1760  df-ral 3108  df-rex 3109

This theorem is referenced by:  reximdv  3233  reximdva  3234  reuind  3673  wefrc  5429  isomin  6944  isofrlem  6947  onfununi  7821  oaordex  8025  odi  8046  omass  8047  omeulem1  8049  noinfep  8958  rankwflemb  9057  infxpenlem  9274  coflim  9518  coftr  9530  zorn2lem7  9759  suplem1pr  10309  axpre-sup  10426  climbdd  14850  filufint  22200  cvati  29822  atcvat4i  29853  mdsymlem2  29860  mdsymlem3  29861  sumdmdii  29871  iccllysconn  32061  dftrpred3g  32626  incsequz2  34502  lcvat  35647  hlrelat3  36029  cvrval3  36030  cvrval4N  36031  2atlt  36056  cvrat4  36060  atbtwnexOLDN  36064  atbtwnex  36065  athgt  36073  2llnmat  36141  lnjatN  36397  2lnat  36401  cdlemb  36411  lhpexle3lem  36628  cdlemf1  37178  cdlemf2  37179  cdlemf  37180  cdlemk26b-3  37522  dvh4dimlem  38060  upbdrech  41066  limcperiod  41405  cncfshift  41652  cncfperiod  41657