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  2836  spc3egv  2896  euind  2991  ssel  3219  reupick  3489  reximdva0m  3508  uniss  3912  eusvnfb  4549  coss1  4883  coss2  4884  ssrelrn  4920  dmss  4928  dmcosseq  5002  funssres  5366  imain  5409  brprcneu  5628  fv3  5658  dffo4  5791  dffo5  5792  f1eqcocnv  5927  mapsn  6854  en2m  6994  ctssdccl  7301  acfun  7412  ccfunen  7473  cc4f  7478  cc4n  7480  dmaddpq  7589  dmmulpq  7590  recexprlemlol  7836  recexprlemupu  7838  ioom  10510  ctinfom  13039  ctinf  13041  omctfn  13054  nninfdclemp1  13061  ptex  13337  subgintm  13775  txcn  14989