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  7292  ccfunen  7349  cc4f  7354  cc4n  7356  dmaddpq  7465  dmmulpq  7466  recexprlemlol  7712  recexprlemupu  7714  ioom  10369  ctinfom  12672  ctinf  12674  omctfn  12687  nninfdclemp1  12694  ptex  12968  subgintm  13406  txcn  14619