Theorem exlimdv 1872

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 1579	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		ax-17 1579	. 2 ⊢ (𝜒 → ∀𝑥𝜒)
3		exlimdv.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	1, 2, 3	exlimdh 1649	1 ⊢ (𝜑 → (∃𝑥𝜓 → 𝜒))

This proof depends on syntax axioms:   → wi 4  ∃wex 1545

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-5 1500  ax-gen 1502  ax-ie2 1547  ax-17 1579

This proof depends on definitions:  df-bi 117

This theorem is used by:  ax11v2  1873  exlimdvv  1953  exlimddv  1954  tpid3g  3828  sssnm  3879  pwntru  4336  euotd  4395  ralxfr2d  4610  rexxfr2d  4611  reldmm  5000  releldmb  5019  relelrnb  5020  elres  5099  iss  5109  imain  5463  elunirn  5972  ovmpt4g  6211  oprssdmm  6405  op1steq  6413  fo2ndf  6463  reldmtpos  6524  rntpos  6528  tfrlemibacc  6597  tfrlemibxssdm  6598  tfrlemibfn  6599  tfrexlem  6605  tfr1onlembacc  6613  tfr1onlembxssdm  6614  tfr1onlembfn  6615  tfrcllembacc  6626  tfrcllembxssdm  6627  tfrcllembfn  6628  map0g  6969  dom1o  7116  xpdom3m  7132  phplem4  7156  phpm  7167  findcard2  7193  findcard2s  7194  ac6sfi  7202  fiintim  7238  xpfi  7239  fidcenum  7273  ordiso  7376  ctmlemr  7448  ctm  7449  ctssdc  7453  pm54.43  7536  exmidfodomrlemim  7553  iftrueb01  7582  pw1m  7583  recclnq  7759  ltexnqq  7775  ltbtwnnqq  7782  recexprlemss1l  8002  recexprlemss1u  8003  negm  10015  ioom  10695  seq3f1olemp  10952  fiinfnf1o  11225  fihashf1rn  11227  hashf1  11287  climcau  12113  summodclem2  12149  zsumdc  12151  isumz  12156  fsumf1o  12157  fisumss  12159  fsumcl2lem  12165  fsumadd  12173  fsummulc2  12215  ntrivcvgap  12315  prodmodclem2  12344  zproddc  12346  prod1dc  12353  fprodf1o  12355  fprodssdc  12357  fprodmul  12358  nnmindc  12811  uzwodc  12814  pceu  13074  4sqlemafi  13174  4sqlem12  13181  ennnfone  13316  enctlem  13323  unct  13333  gzsumfzval  13711  sgrpidmndm  13733  gsumvalfi  14152  subrngintm  14520  subrgintm  14551  islssm  14694  lss0cl  14706  islidlm  14816  eltg3  15158  tgtop  15169  tgidm  15175  tgrest  15270  tgcn  15309  xblm  15518  dvfgg  15789  dvcnp2cntop  15800  2lgslem1  16210  pwtrufal  17027