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  3908  eusvnfb  4544  coss1  4876  coss2  4877  ssrelrn  4913  dmss  4921  dmcosseq  4995  funssres  5359  imain  5402  brprcneu  5619  fv3  5649  dffo4  5782  dffo5  5783  f1eqcocnv  5914  mapsn  6835  en2m  6972  ctssdccl  7274  acfun  7385  ccfunen  7446  cc4f  7451  cc4n  7453  dmaddpq  7562  dmmulpq  7563  recexprlemlol  7809  recexprlemupu  7811  ioom  10475  ctinfom  12994  ctinf  12996  omctfn  13009  nninfdclemp1  13016  ptex  13292  subgintm  13730  txcn  14943