Theorem eximdv 1833

Description: Deduction form of Theorem 19.22 of [Margaris] p. 90, see exim 1751. (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-5 1827	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		alimdv.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	eximdh 1778	1 ⊢ (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))

Syntax hints:   → wi 4  ∃wex 1695

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827

This theorem depends on definitions:  df-bi 196  df-ex 1696

This theorem is referenced by:  2eximdv  1835  exlimdv  1848  19.41v  1901  equvinv  1946  equviniva  1947  equvinivOLD  1948  mo2v  2465  moim  2507  reximdv2  2997  cgsexg  3211  spc3egv  3270  euind  3360  ssel  3562  reupick  3870  reximdva0  3891  uniss  4394  eusvnfb  4788  reusv2lem3  4797  relopabi  5167  coss1  5199  coss2  5200  ssrelrn  5237  dmss  5245  dmcosseq  5308  funssres  5844  brprcneu  6096  fv3  6116  dffv2  6181  fvn0ssdmfun  6258  dffo4  6283  dffo5  6284  funopsn  6319  fvclss  6404  fsnex  6438  f1prex  6439  f1eqcocnv  6456  mapsn  7785  enp1i  8080  en2  8081  en4  8083  marypha2  8228  brwdom3  8370  isinffi  8701  infpwfien  8768  infmap2  8923  cfub  8954  cflm  8955  cff1  8963  cfss  8970  isf32lem9  9066  axcc4  9144  acncc  9145  domtriomlem  9147  ac6s  9189  iundom2g  9241  winalim2  9397  grudomon  9518  nsmallnq  9678  prnmadd  9698  ltexprlem1  9737  ltexprlem3  9739  ltexprlem4  9740  reclem2pr  9749  dedekind  10079  xrsupsslem  12009  xrinfmsslem  12010  ishashinf  13104  coss12d  13559  supcvg  14427  vdwlem2  15524  ram0  15564  mreexexlem2d  16128  initoeu1  16484  termoeu1  16491  acsmapd  17001  acsmap2d  17002  dirge  17060  odcau  17842  ablfac2  18311  lspprat  18974  cmpsub  21013  cmpcld  21015  2ndcsep  21072  1stcelcls  21074  txcn  21239  fgcl  21492  ufildom1  21540  metustexhalf  22171  bcthlem5  22933  mbfi1flim  23296  itg2seq  23315  dchrisumlem3  24980  upgrex  25759  umgraex  25852  usgraedg4  25916  wlklniswwlkn2  26228  frisusgranb  26524  frgrancvvdeqlemC  26566  ubthlem1  27110  axhcompl-zf  27239  isch3  27482  cnlnssadj  28323  acunirnmpt  28841  f1ocnt  28946  insiga  29527  bnj605  30231  bnj607  30240  bnj1018  30286  erdsze2lem1  30439  fundmpss  30910  bj-restn0  32224  dissneqlem  32363  relowlpssretop  32388  poimirlem30  32609  fdc1  32712  prdstotbnd  32763  prter2  33184  lsat0cv  33338  pmapglb2N  34075  elpaddn0  34104  cdlemftr3  34871  dibglbN  35473  dihglbcpreN  35607  dihjatcclem4  35728  mapdordlem2  35944  dfac11  36650  neik0pk1imk0  37365  ax6e2ndeq  37796  fnchoice  38211  rfcnnnub  38218  eliin2f  38316  founiiun0  38372  mapsnd  38383  axccd  38424  axccd2  38425  fzisoeu  38455  islpcn  38706  lptre2pt  38707  stoweidlem14  38907  stoweidlem35  38928  stoweidlem39  38932  stoweidlem50  38943  stoweidlem56  38949  stoweidlem59  38952  stoweidlem60  38953  fourier2  39120  qndenserrnbllem  39190  qndenserrn  39195  ovncvrrp  39454  ovnsubaddlem2  39461  hoidmvval0b  39480  hoiqssbllem3  39514  funressnfv  39857  uhgrvd00  40750  1wlkiswwlksupgr2  41074  1wlklnwwlkln2lem  41079  umgrwwlks2on  41161  wpthswwlks2on  41164  frcond3  41440  frgrncvvdeqlemC  41478