Theorem reximdvai 3191

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

Syntax hints:   → wi 4   ∈ wcel 2110  ∀wral 3061  ∃wrex 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-ral 3066  df-rex 3067

This theorem is referenced by:  reximdv  3192  reximdva  3193  reuind  3666  wefrc  5545  isomin  7146  isofrlem  7149  onfununi  8078  oaordex  8286  odi  8307  omass  8308  omeulem1  8310  noinfep  9275  dftrpred3g  9339  rankwflemb  9409  infxpenlem  9627  coflim  9875  coftr  9887  zorn2lem7  10116  suplem1pr  10666  axpre-sup  10783  climbdd  15235  filufint  22817  cvati  30447  atcvat4i  30478  mdsymlem2  30485  mdsymlem3  30486  sumdmdii  30496  iccllysconn  32925  incsequz2  35644  lcvat  36781  hlrelat3  37163  cvrval3  37164  cvrval4N  37165  2atlt  37190  cvrat4  37194  atbtwnexOLDN  37198  atbtwnex  37199  athgt  37207  2llnmat  37275  lnjatN  37531  2lnat  37535  cdlemb  37545  lhpexle3lem  37762  cdlemf1  38312  cdlemf2  38313  cdlemf  38314  cdlemk26b-3  38656  dvh4dimlem  39194  upbdrech  42517  limcperiod  42844  cncfshift  43090  cncfperiod  43095