Theorem exlimdv 1833

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 1540	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		ax-17 1540	. 2 ⊢ (𝜒 → ∀𝑥𝜒)
3		exlimdv.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	1, 2, 3	exlimdh 1610	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-5 1461  ax-gen 1463  ax-ie2 1508  ax-17 1540

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11v2  1834  exlimdvv  1912  exlimddv  1913  tpid3g  3738  sssnm  3785  pwntru  4233  euotd  4288  ralxfr2d  4500  rexxfr2d  4501  releldmb  4904  relelrnb  4905  elres  4983  iss  4993  imain  5341  elunirn  5816  ovmpt4g  6049  oprssdmm  6238  op1steq  6246  fo2ndf  6294  reldmtpos  6320  rntpos  6324  tfrlemibacc  6393  tfrlemibxssdm  6394  tfrlemibfn  6395  tfrexlem  6401  tfr1onlembacc  6409  tfr1onlembxssdm  6410  tfr1onlembfn  6411  tfrcllembacc  6422  tfrcllembxssdm  6423  tfrcllembfn  6424  map0g  6756  xpdom3m  6902  phplem4  6925  phpm  6935  findcard2  6959  findcard2s  6960  ac6sfi  6968  fiintim  7001  xpfi  7002  fidcenum  7031  ordiso  7111  ctmlemr  7183  ctm  7184  ctssdc  7188  pm54.43  7271  exmidfodomrlemim  7282  recclnq  7478  ltexnqq  7494  ltbtwnnqq  7501  recexprlemss1l  7721  recexprlemss1u  7722  negm  9708  ioom  10369  seq3f1olemp  10626  fiinfnf1o  10897  fihashf1rn  10899  climcau  11531  summodclem2  11566  zsumdc  11568  isumz  11573  fsumf1o  11574  fisumss  11576  fsumcl2lem  11582  fsumadd  11590  fsummulc2  11632  ntrivcvgap  11732  prodmodclem2  11761  zproddc  11763  prod1dc  11770  fprodf1o  11772  fprodssdc  11774  fprodmul  11775  nnmindc  12228  uzwodc  12231  pceu  12491  4sqlemafi  12591  4sqlem12  12598  ennnfone  12669  enctlem  12676  unct  12686  gsumfzval  13095  sgrpidmndm  13124  subrngintm  13846  subrgintm  13877  islssm  13991  lss0cl  14003  islidlm  14113  eltg3  14401  tgtop  14412  tgidm  14418  tgrest  14513  tgcn  14552  xblm  14761  dvfgg  15032  dvcnp2cntop  15043  2lgslem1  15440  pwtrufal  15752