Theorem eximdv 1920

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

Syntax hints:   → wi 4  ∃wex 1781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913

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

This theorem is referenced by:  2eximdv  1922  exlimdv  1936  19.41v  1953  equvinva  2033  dfmoeu  2529  moim  2537  mo4  2559  reximdv2  3157  cgsexg  3489  spcimdv  3553  spcegv  3557  euind  3685  sbcimdv  3816  sselOLD  3941  reupick  4283  reximdva0  4316  uniss  4878  dfiun2g  4995  eusvnfb  5353  reusv2lem3  5360  axprlem1  5383  axprlem2  5384  axprlem3  5385  axpr  5388  exexneq  5396  relopabi  5783  coss1  5816  coss2  5817  ssrelrn  5855  dmss  5863  dmcosseq  5933  funssres  6550  brprcneu  6837  brprcneuALT  6838  fv3  6865  dffv2  6941  fvn0ssdmfun  7030  dffo4  7058  dffo5  7059  funopsn  7099  fvclss  7194  fsnex  7234  f1prex  7235  f1eqcocnv  7252  f1eqcocnvOLD  7253  mapsnd  8831  enp1iOLD  9231  en2  9232  en4  9234  marypha2  9384  brwdom3  9527  isinffi  9937  infpwfien  10007  infmap2  10163  cfub  10194  cflm  10195  cff1  10203  cfss  10210  isf32lem9  10306  axcc4  10384  acncc  10385  domtriomlem  10387  ac6s  10429  iundom2g  10485  winalim2  10641  grudomon  10762  nsmallnq  10922  prnmadd  10942  ltexprlem1  10981  ltexprlem3  10983  ltexprlem4  10984  reclem2pr  10993  dedekind  11327  xrsupsslem  13236  xrinfmsslem  13237  ishashinf  14374  coss12d  14869  supcvg  15752  vdwlem2  16865  ram0  16905  mreexexlem2d  17539  initoeu1  17911  termoeu1  17918  acsmapd  18457  acsmap2d  18458  dirge  18506  odcau  19400  ablfac2  19882  lspprat  20673  cmpsub  22788  cmpcld  22790  2ndcsep  22847  1stcelcls  22849  txcn  23014  fgcl  23266  ufildom1  23314  metustexhalf  23949  bcthlem5  24729  mbfi1flim  25125  itg2seq  25144  dchrisumlem3  26876  upgrex  28106  uhgrvd00  28545  wlkiswwlksupgr2  28885  wlklnwwlkln2lem  28890  umgrwwlks2on  28965  wpthswwlks2on  28969  frcond3  29276  frgrncvvdeqlem9  29314  ubthlem1  29875  axhcompl-zf  30003  isch3  30246  cnlnssadj  31085  acunirnmpt  31642  f1ocnt  31773  qsxpid  32222  zarclsint  32542  insiga  32825  bnj605  33608  bnj607  33617  bnj1018g  33664  bnj1018  33665  cusgredgex  33802  loop1cycl  33818  erdsze2lem1  33884  fundmpss  34427  bj-zfauscl  35467  bj-restn0  35634  dissneqlem  35884  relowlpssretop  35908  pibt2  35961  poimirlem30  36181  fdc1  36278  prdstotbnd  36326  cossss  36960  prter2  37416  lsat0cv  37568  pmapglb2N  38307  elpaddn0  38336  cdlemftr3  39101  dibglbN  39702  dihglbcpreN  39836  dihjatcclem4  39957  mapdordlem2  40173  sticksstones3  40629  sticksstones20  40647  sn-axprlem3  40710  dfac11  41447  neik0pk1imk0  42441  rr-spce  42599  cpcolld  42660  ismnushort  42703  ax6e2ndeq  42963  fnchoice  43356  rfcnnnub  43363  eliin2f  43436  founiiun0  43531  disjinfi  43534  axccd  43571  axccd2  43572  fvelima2  43609  fzisoeu  43655  islpcn  44000  lptre2pt  44001  stoweidlem14  44375  stoweidlem35  44396  stoweidlem39  44400  stoweidlem50  44411  stoweidlem56  44417  stoweidlem59  44420  stoweidlem60  44421  fourier2  44588  qndenserrnbllem  44655  qndenserrn  44660  ovncvrrp  44925  ovnsubaddlem2  44932  hoidmvval0b  44951  hoiqssbllem3  44985  natlocalincr  45235  tworepnotupword  45245  funressnfv  45397  imasetpreimafvbijlemfv1  45715  fundcmpsurinjpreimafv  45720  elsprel  45787  subthinc  47180