Theorem eximdv 1924

Description: Deduction form of Theorem 19.22 of [Margaris] p. 90, see exim 1841. See eximdh 1871 and eximd 2228 for versions without a distinct variable condition. (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 1917	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		alimdv.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	eximdh 1871	1 ⊢ (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))

Syntax hints:   → wi 4  ∃wex 1786

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917

This theorem depends on definitions:  df-bi 208  df-ex 1787

This theorem is referenced by:  2eximdv  1926  exlimdv  1940  19.41v  1956  equvinva  2037  dfmoeu  2539  moim  2548  mo4  2570  reximdv2  3149  cgsexg  3475  spcimdv  3531  spcegv  3535  euind  3665  sbcimdv  3791  reupick  4257  reximdva0  4283  uniss  4846  dfiun2g  4959  replem  5210  sepexlem  5221  eusvnfb  5322  reusv2lem3  5329  axprlem2  5353  axprlem4  5355  axpr  5356  axprlem1OLD  5357  axprlem3OLD  5358  axprOLD  5361  axprglem  5365  exexneq  5374  relopabi  5765  coss1  5797  coss2  5798  ssrelrn  5836  dmss  5844  dmcosseq  5920  dmcosseqOLD  5921  dmcosseqOLDOLD  5922  funssres  6529  brprcneu  6817  brprcneuALT  6818  fv3  6845  fvelima2  6879  dffv2  6922  fvn0ssdmfun  7015  dffo4  7044  dffo5  7045  funopsn  7090  funopsnOLD  7091  fvclss  7185  fsnex  7227  f1prex  7228  f1eqcocnv  7245  mapsnd  8824  en2  9180  en4  9182  marypha2  9342  brwdom3  9487  elirrvOLD  9503  isinffi  9907  infpwfien  9975  infmap2  10130  cfub  10162  cflm  10163  cff1  10171  cfss  10178  isf32lem9  10274  axcc4  10352  acncc  10353  domtriomlem  10355  ac6s  10397  iundom2g  10453  winalim2  10610  grudomon  10731  nsmallnq  10891  prnmadd  10911  ltexprlem1  10950  ltexprlem3  10952  ltexprlem4  10953  reclem2pr  10962  dedekind  11300  xrsupsslem  13250  xrinfmsslem  13251  ishashinf  14416  hash3tpde  14446  coss12d  14925  supcvg  15812  vdwlem2  16944  ram0  16984  mreexexlem2d  17602  initoeu1  17969  termoeu1  17976  acsmapd  18511  acsmap2d  18512  dirge  18560  odcau  19570  ablfac2  20057  lspprat  21146  cmpsub  23383  cmpcld  23385  2ndcsep  23442  1stcelcls  23444  txcn  23609  fgcl  23861  ufildom1  23909  metustexhalf  24539  bcthlem5  25313  mbfi1flim  25708  itg2seq  25727  dchrisumlem3  27472  upgrex  29179  uhgrvd00  29621  wlkiswwlksupgr2  29963  wlklnwwlkln2lem  29968  usgrwwlks2on  30044  umgrwwlks2on  30045  wpthswwlks2on  30050  frcond3  30357  frgrncvvdeqlem9  30395  ubthlem1  30959  axhcompl-zf  31087  isch3  31330  cnlnssadj  32169  ac6mapd  32715  acunirnmpt  32751  padct  32810  f1ocnt  32892  wrdpmtrlast  33174  qsxpid  33445  zarclsint  34056  insiga  34321  bnj605  35089  bnj607  35098  bnj1018g  35145  bnj1018  35146  axprALT2  35290  axsepg2  35321  axsepg4  35324  axpowg2  35328  cusgredgex  35350  loop1cycl  35365  erdsze2lem1  35431  fundmpss  35995  axtco1from2  36703  regsfromregtco  36766  bj-zfauscl  37277  bj-axseprep  37427  bj-restn0  37448  dissneqlem  37702  relowlpssretop  37726  pibt2  37779  wl-isseteq  37867  wl-dfcleq  37876  poimirlem30  38017  fdc1  38113  prdstotbnd  38161  cossss  38882  prter2  39373  lsat0cv  39525  pmapglb2N  40263  elpaddn0  40292  cdlemftr3  41057  dibglbN  41658  dihglbcpreN  41792  dihjatcclem4  41913  sticksstones3  42633  sticksstones20  42651  sn-axprlem3  42705  eu6w  43126  dfac11  43507  neik0pk1imk0  44491  rr-spce  44648  cpcolld  44702  ismnushort  44745  ax6e2ndeq  45003  ssclaxsep  45426  fnchoice  45477  rfcnnnub  45484  eliin2f  45551  founiiun0  45637  disjinfi  45639  axccd  45673  axccd2  45674  fzisoeu  45748  islpcn  46082  lptre2pt  46083  stoweidlem14  46457  stoweidlem35  46478  stoweidlem39  46482  stoweidlem50  46493  stoweidlem56  46499  stoweidlem59  46502  stoweidlem60  46503  fourier2  46670  qndenserrnbllem  46737  qndenserrn  46742  ovncvrrp  47007  ovnsubaddlem2  47014  hoidmvval0b  47033  hoiqssbllem3  47067  ormklocald  47319  natlocalincr  47321  funressnfv  47506  imasetpreimafvbijlemfv1  47878  fundcmpsurinjpreimafv  47883  elsprel  47950  isubgredg  48357  isubgr3stgr  48466  grlimedgclnbgr  48486  grlimprclnbgredg  48488  grlimpredg  48489  grlimprclnbgrvtx  48490  grilcbri2  48502  clnbgr3stgrgrlic  48511  subthinc  49933