Theorem exlimdv 1791

Description: Deduction from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 27-Apr-1994.)

Hypothesis

Ref	Expression
exlimdv.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
exlimdv	⊢ (𝜑 → (∃𝑥𝜓 → 𝜒))

Distinct variable groups:   𝜒,𝑥   𝜑,𝑥

Allowed substitution hint:   𝜓(𝑥)

Proof of Theorem exlimdv

Step	Hyp	Ref	Expression
1		ax-17 1506	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		ax-17 1506	. 2 ⊢ (𝜒 → ∀𝑥𝜒)
3		exlimdv.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	1, 2, 3	exlimdh 1575	1 ⊢ (𝜑 → (∃𝑥𝜓 → 𝜒))

Syntax hints:   → wi 4  ∃wex 1468

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-5 1423  ax-gen 1425  ax-ie2 1470  ax-17 1506

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  ax11v2  1792  exlimdvv  1869  exlimddv  1870  tpid3g  3638  sssnm  3681  pwntru  4122  euotd  4176  ralxfr2d  4385  rexxfr2d  4386  releldmb  4776  relelrnb  4777  elres  4855  iss  4865  imain  5205  elunirn  5667  ovmpt4g  5893  oprssdmm  6069  op1steq  6077  fo2ndf  6124  reldmtpos  6150  rntpos  6154  tfrlemibacc  6223  tfrlemibxssdm  6224  tfrlemibfn  6225  tfrexlem  6231  tfr1onlembacc  6239  tfr1onlembxssdm  6240  tfr1onlembfn  6241  tfrcllembacc  6252  tfrcllembxssdm  6253  tfrcllembfn  6254  map0g  6582  xpdom3m  6728  phplem4  6749  phpm  6759  findcard2  6783  findcard2s  6784  ac6sfi  6792  fiintim  6817  xpfi  6818  fidcenum  6844  ordiso  6921  ctmlemr  6993  ctm  6994  ctssdc  6998  pm54.43  7046  exmidfodomrlemim  7057  recclnq  7200  ltexnqq  7216  ltbtwnnqq  7223  recexprlemss1l  7443  recexprlemss1u  7444  negm  9407  ioom  10038  seq3f1olemp  10275  fiinfnf1o  10532  fihashf1rn  10535  climcau  11116  summodclem2  11151  zsumdc  11153  isumz  11158  fsumf1o  11159  fisumss  11161  fsumcl2lem  11167  fsumadd  11175  fsummulc2  11217  ntrivcvgap  11317  prodmodclem2  11346  ennnfone  11938  enctlem  11945  unct  11954  eltg3  12226  tgtop  12237  tgidm  12243  tgrest  12338  tgcn  12377  xblm  12586  dvfgg  12826  dvcnp2cntop  12832  pwtrufal  13192