Theorem eximdv 1902

Description: Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 27-Apr-1994.)

Hypothesis

Ref	Expression
alimdv.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
eximdv	⊢ (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)

Proof of Theorem eximdv

Step	Hyp	Ref	Expression
1		ax-17 1548	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		alimdv.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	eximdh 1633	1 ⊢ (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))

Syntax hints:   → wi 4  ∃wex 1514

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1469  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-4 1532  ax-17 1548  ax-ial 1556

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  2eximdv  1904  reximdv2  2604  cgsexg  2806  spc3egv  2864  euind  2959  ssel  3186  reupick  3456  reximdva0m  3475  uniss  3870  eusvnfb  4500  coss1  4832  coss2  4833  dmss  4876  dmcosseq  4949  funssres  5312  imain  5355  brprcneu  5568  fv3  5598  dffo4  5727  dffo5  5728  f1eqcocnv  5859  mapsn  6776  ctssdccl  7212  acfun  7318  ccfunen  7375  cc4f  7380  cc4n  7382  dmaddpq  7491  dmmulpq  7492  recexprlemlol  7738  recexprlemupu  7740  ioom  10401  ctinfom  12770  ctinf  12772  omctfn  12785  nninfdclemp1  12792  ptex  13067  subgintm  13505  txcn  14718