Theorem eximdv 1921

Description: Deduction form of Theorem 19.22 of [Margaris] p. 90, see exim 1837. See eximdh 1868 and eximd 2212 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 1914	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		alimdv.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	eximdh 1868	1 ⊢ (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))

Syntax hints:   → wi 4  ∃wex 1783

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-ex 1784

This theorem is referenced by:  2eximdv  1923  exlimdv  1937  19.41v  1954  equvinva  2034  dfmoeu  2536  moim  2544  mo4  2566  reximdv2  3198  cgsexg  3464  spcimdv  3522  spcegv  3526  euind  3654  sbcimdv  3786  sselOLD  3911  reupick  4249  reximdva0  4282  uniss  4844  eusvnfb  5311  reusv2lem3  5318  axprlem1  5341  axprlem2  5342  axprlem3  5343  axpr  5346  relopabi  5721  coss1  5753  coss2  5754  ssrelrn  5792  dmss  5800  dmcosseq  5871  funssres  6462  brprcneu  6747  fvprc  6748  fv3  6774  dffv2  6845  fvn0ssdmfun  6934  dffo4  6961  dffo5  6962  funopsn  7002  fvclss  7097  fsnex  7135  f1prex  7136  f1eqcocnv  7153  f1eqcocnvOLD  7154  mapsnd  8632  enp1i  8982  en2  8983  en4  8985  marypha2  9128  brwdom3  9271  isinffi  9681  infpwfien  9749  infmap2  9905  cfub  9936  cflm  9937  cff1  9945  cfss  9952  isf32lem9  10048  axcc4  10126  acncc  10127  domtriomlem  10129  ac6s  10171  iundom2g  10227  winalim2  10383  grudomon  10504  nsmallnq  10664  prnmadd  10684  ltexprlem1  10723  ltexprlem3  10725  ltexprlem4  10726  reclem2pr  10735  dedekind  11068  xrsupsslem  12970  xrinfmsslem  12971  ishashinf  14105  coss12d  14611  supcvg  15496  vdwlem2  16611  ram0  16651  mreexexlem2d  17271  initoeu1  17642  termoeu1  17649  acsmapd  18187  acsmap2d  18188  dirge  18236  odcau  19124  ablfac2  19607  lspprat  20330  cmpsub  22459  cmpcld  22461  2ndcsep  22518  1stcelcls  22520  txcn  22685  fgcl  22937  ufildom1  22985  metustexhalf  23618  bcthlem5  24397  mbfi1flim  24793  itg2seq  24812  dchrisumlem3  26544  upgrex  27365  uhgrvd00  27804  wlkiswwlksupgr2  28143  wlklnwwlkln2lem  28148  umgrwwlks2on  28223  wpthswwlks2on  28227  frcond3  28534  frgrncvvdeqlem9  28572  ubthlem1  29133  axhcompl-zf  29261  isch3  29504  cnlnssadj  30343  acunirnmpt  30898  f1ocnt  31025  qsxpid  31460  zarclsint  31724  insiga  32005  bnj605  32787  bnj607  32796  bnj1018g  32843  bnj1018  32844  cusgredgex  32983  loop1cycl  32999  erdsze2lem1  33065  fundmpss  33646  bj-zfauscl  35039  bj-restn0  35188  dissneqlem  35438  relowlpssretop  35462  pibt2  35515  poimirlem30  35734  fdc1  35831  prdstotbnd  35879  cossss  36475  prter2  36822  lsat0cv  36974  pmapglb2N  37712  elpaddn0  37741  cdlemftr3  38506  dibglbN  39107  dihglbcpreN  39241  dihjatcclem4  39362  mapdordlem2  39578  sticksstones3  40032  sticksstones20  40050  sn-axprlem3  40114  sn-dtru  40116  dfac11  40803  neik0pk1imk0  41546  rr-spce  41704  cpcolld  41765  ismnushort  41808  ax6e2ndeq  42068  fnchoice  42461  rfcnnnub  42468  eliin2f  42543  founiiun0  42617  disjinfi  42620  axccd  42657  axccd2  42658  fvelima2  42695  fzisoeu  42729  islpcn  43070  lptre2pt  43071  stoweidlem14  43445  stoweidlem35  43466  stoweidlem39  43470  stoweidlem50  43481  stoweidlem56  43487  stoweidlem59  43490  stoweidlem60  43491  fourier2  43658  qndenserrnbllem  43725  qndenserrn  43730  ovncvrrp  43992  ovnsubaddlem2  43999  hoidmvval0b  44018  hoiqssbllem3  44052  funressnfv  44424  imasetpreimafvbijlemfv1  44743  fundcmpsurinjpreimafv  44748  elsprel  44815  subthinc  46209