Theorem eximdv 1917

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

Syntax hints:   → wi 4  ∃wex 1779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-ex 1780

This theorem is referenced by:  2eximdv  1919  exlimdv  1933  19.41v  1949  equvinva  2030  dfmoeu  2536  moim  2544  mo4  2566  reximdv2  3151  cgsexg  3510  spcimdv  3577  spcegv  3581  euind  3712  sbcimdv  3839  reupick  4309  reximdva0  4335  uniss  4896  dfiun2g  5011  sepexlem  5274  eusvnfb  5368  reusv2lem3  5375  axprlem1  5398  axprlem2  5399  axprlem4  5401  axpr  5402  axprlem3OLD  5403  axprOLD  5406  exexneq  5414  relopabi  5806  coss1  5840  coss2  5841  ssrelrn  5879  dmss  5887  dmcosseq  5961  dmcosseqOLD  5962  funssres  6585  brprcneu  6871  brprcneuALT  6872  fv3  6899  fvelima2  6936  dffv2  6979  fvn0ssdmfun  7069  dffo4  7098  dffo5  7099  funopsn  7143  fvclss  7238  fsnex  7281  f1prex  7282  f1eqcocnv  7299  mapsnd  8905  enp1iOLD  9291  en2  9292  en4  9294  marypha2  9456  brwdom3  9601  isinffi  10011  infpwfien  10081  infmap2  10236  cfub  10268  cflm  10269  cff1  10277  cfss  10284  isf32lem9  10380  axcc4  10458  acncc  10459  domtriomlem  10461  ac6s  10503  iundom2g  10559  winalim2  10715  grudomon  10836  nsmallnq  10996  prnmadd  11016  ltexprlem1  11055  ltexprlem3  11057  ltexprlem4  11058  reclem2pr  11067  dedekind  11403  xrsupsslem  13328  xrinfmsslem  13329  ishashinf  14486  hash3tpde  14516  coss12d  14996  supcvg  15877  vdwlem2  17007  ram0  17047  mreexexlem2d  17662  initoeu1  18029  termoeu1  18036  acsmapd  18569  acsmap2d  18570  dirge  18618  odcau  19590  ablfac2  20077  lspprat  21119  cmpsub  23343  cmpcld  23345  2ndcsep  23402  1stcelcls  23404  txcn  23569  fgcl  23821  ufildom1  23869  metustexhalf  24500  bcthlem5  25285  mbfi1flim  25681  itg2seq  25700  dchrisumlem3  27459  upgrex  29076  uhgrvd00  29519  wlkiswwlksupgr2  29864  wlklnwwlkln2lem  29869  umgrwwlks2on  29944  wpthswwlks2on  29948  frcond3  30255  frgrncvvdeqlem9  30293  ubthlem1  30856  axhcompl-zf  30984  isch3  31227  cnlnssadj  32066  ac6mapd  32608  acunirnmpt  32642  f1ocnt  32784  wrdpmtrlast  33109  qsxpid  33382  zarclsint  33908  insiga  34173  bnj605  34943  bnj607  34952  bnj1018g  34999  bnj1018  35000  cusgredgex  35149  loop1cycl  35164  erdsze2lem1  35230  fundmpss  35789  bj-zfauscl  36947  bj-restn0  37113  dissneqlem  37363  relowlpssretop  37387  pibt2  37440  wl-isseteq  37528  poimirlem30  37679  fdc1  37775  prdstotbnd  37823  cossss  38448  prter2  38904  lsat0cv  39056  pmapglb2N  39795  elpaddn0  39824  cdlemftr3  40589  dibglbN  41190  dihglbcpreN  41324  dihjatcclem4  41445  mapdordlem2  41661  sticksstones3  42166  sticksstones20  42184  sn-axprlem3  42235  eu6w  42674  dfac11  43061  neik0pk1imk0  44046  rr-spce  44203  cpcolld  44257  ismnushort  44300  ax6e2ndeq  44559  ssclaxsep  44982  fnchoice  45033  rfcnnnub  45040  eliin2f  45108  founiiun0  45194  disjinfi  45196  axccd  45233  axccd2  45234  fzisoeu  45309  islpcn  45648  lptre2pt  45649  stoweidlem14  46023  stoweidlem35  46044  stoweidlem39  46048  stoweidlem50  46059  stoweidlem56  46065  stoweidlem59  46068  stoweidlem60  46069  fourier2  46236  qndenserrnbllem  46303  qndenserrn  46308  ovncvrrp  46573  ovnsubaddlem2  46580  hoidmvval0b  46599  hoiqssbllem3  46633  ormklocald  46883  natlocalincr  46885  tworepnotupword  46895  funressnfv  47052  imasetpreimafvbijlemfv1  47397  fundcmpsurinjpreimafv  47402  elsprel  47469  isubgredg  47859  isubgr3stgr  47967  grilcbri2  47996  clnbgr3stgrgrlic  48004  subthinc  49309