Theorem eximdv 1926

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

Syntax hints:   → wi 4  ∃wex 1538

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  2eximdv  1928  reximdv2  2629  cgsexg  2835  spc3egv  2895  euind  2990  ssel  3218  reupick  3488  reximdva0m  3507  uniss  3909  eusvnfb  4545  coss1  4877  coss2  4878  ssrelrn  4914  dmss  4922  dmcosseq  4996  funssres  5360  imain  5403  brprcneu  5622  fv3  5652  dffo4  5785  dffo5  5786  f1eqcocnv  5921  mapsn  6845  en2m  6982  ctssdccl  7289  acfun  7400  ccfunen  7461  cc4f  7466  cc4n  7468  dmaddpq  7577  dmmulpq  7578  recexprlemlol  7824  recexprlemupu  7826  ioom  10492  ctinfom  13014  ctinf  13016  omctfn  13029  nninfdclemp1  13036  ptex  13312  subgintm  13750  txcn  14964