Theorem eximdv 1894

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

Syntax hints:   → wi 4  ∃wex 1506

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  2eximdv  1896  reximdv2  2596  cgsexg  2798  spc3egv  2856  euind  2951  ssel  3178  reupick  3448  reximdva0m  3467  uniss  3861  eusvnfb  4490  coss1  4822  coss2  4823  dmss  4866  dmcosseq  4938  funssres  5301  imain  5341  brprcneu  5554  fv3  5584  dffo4  5713  dffo5  5714  f1eqcocnv  5841  mapsn  6758  ctssdccl  7186  acfun  7290  ccfunen  7347  cc4f  7352  cc4n  7354  dmaddpq  7463  dmmulpq  7464  recexprlemlol  7710  recexprlemupu  7712  ioom  10367  ctinfom  12670  ctinf  12672  omctfn  12685  nninfdclemp1  12692  ptex  12966  subgintm  13404  txcn  14595