Theorem eximdv 1929

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 1575	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		alimdv.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	eximdh 1660	1 ⊢ (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))

Syntax hints:   → wi 4  ∃wex 1541

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  2eximdv  1931  reximdv2  2641  cgsexg  2849  spc3egv  2909  euind  3004  ssel  3232  reupick  3505  reximdva0m  3524  uniss  3935  eusvnfb  4575  coss1  4910  coss2  4911  ssrelrn  4947  dmss  4955  dmcosseq  5029  funssres  5395  imain  5438  brprcneu  5663  fv3  5693  dffo4  5825  dffo5  5826  f1eqcocnv  5964  mapsnd  6923  mapsn  6925  en2m  7066  ctssdccl  7402  acfun  7514  ccfunen  7578  cc4f  7583  cc4n  7585  dmaddpq  7694  dmmulpq  7695  recexprlemlol  7941  recexprlemupu  7943  ioom  10620  ctinfom  13179  ctinf  13181  omctfn  13194  nninfdclemp1  13201  ptex  13477  subgintm  13915  txcn  15140