Theorem eximdv 1917

Description: Deduction form of Theorem 19.22 of [Margaris] p. 90, see exim 1834. See eximdh 1864 and eximd 2216 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  2029  dfmoeu  2536  moim  2544  mo4  2566  reximdv2  3164  cgsexg  3526  spcimdv  3593  spcegv  3597  euind  3730  sbcimdv  3859  reupick  4329  reximdva0  4355  uniss  4915  dfiun2g  5030  sepexlem  5299  eusvnfb  5393  reusv2lem3  5400  axprlem1  5423  axprlem2  5424  axprlem4  5426  axpr  5427  axprlem3OLD  5428  axprOLD  5431  exexneq  5439  relopabi  5832  coss1  5866  coss2  5867  ssrelrn  5905  dmss  5913  dmcosseq  5987  dmcosseqOLD  5988  funssres  6610  brprcneu  6896  brprcneuALT  6897  fv3  6924  fvelima2  6961  dffv2  7004  fvn0ssdmfun  7094  dffo4  7123  dffo5  7124  funopsn  7168  fvclss  7261  fsnex  7303  f1prex  7304  f1eqcocnv  7321  mapsnd  8926  enp1iOLD  9314  en2  9315  en4  9317  marypha2  9479  brwdom3  9622  isinffi  10032  infpwfien  10102  infmap2  10257  cfub  10289  cflm  10290  cff1  10298  cfss  10305  isf32lem9  10401  axcc4  10479  acncc  10480  domtriomlem  10482  ac6s  10524  iundom2g  10580  winalim2  10736  grudomon  10857  nsmallnq  11017  prnmadd  11037  ltexprlem1  11076  ltexprlem3  11078  ltexprlem4  11079  reclem2pr  11088  dedekind  11424  xrsupsslem  13349  xrinfmsslem  13350  ishashinf  14502  hash3tpde  14532  coss12d  15011  supcvg  15892  vdwlem2  17020  ram0  17060  mreexexlem2d  17688  initoeu1  18056  termoeu1  18063  acsmapd  18599  acsmap2d  18600  dirge  18648  odcau  19622  ablfac2  20109  lspprat  21155  cmpsub  23408  cmpcld  23410  2ndcsep  23467  1stcelcls  23469  txcn  23634  fgcl  23886  ufildom1  23934  metustexhalf  24569  bcthlem5  25362  mbfi1flim  25758  itg2seq  25777  dchrisumlem3  27535  upgrex  29109  uhgrvd00  29552  wlkiswwlksupgr2  29897  wlklnwwlkln2lem  29902  umgrwwlks2on  29977  wpthswwlks2on  29981  frcond3  30288  frgrncvvdeqlem9  30326  ubthlem1  30889  axhcompl-zf  31017  isch3  31260  cnlnssadj  32099  ac6mapd  32635  acunirnmpt  32669  f1ocnt  32804  wrdpmtrlast  33113  qsxpid  33390  zarclsint  33871  insiga  34138  bnj605  34921  bnj607  34930  bnj1018g  34977  bnj1018  34978  cusgredgex  35127  loop1cycl  35142  erdsze2lem1  35208  fundmpss  35767  bj-zfauscl  36925  bj-restn0  37091  dissneqlem  37341  relowlpssretop  37365  pibt2  37418  wl-isseteq  37506  poimirlem30  37657  fdc1  37753  prdstotbnd  37801  cossss  38426  prter2  38882  lsat0cv  39034  pmapglb2N  39773  elpaddn0  39802  cdlemftr3  40567  dibglbN  41168  dihglbcpreN  41302  dihjatcclem4  41423  mapdordlem2  41639  sticksstones3  42149  sticksstones20  42167  sn-axprlem3  42256  eu6w  42686  dfac11  43074  neik0pk1imk0  44060  rr-spce  44217  cpcolld  44277  ismnushort  44320  ax6e2ndeq  44579  ssclaxsep  44999  fnchoice  45034  rfcnnnub  45041  eliin2f  45109  founiiun0  45195  disjinfi  45197  axccd  45234  axccd2  45235  fzisoeu  45312  islpcn  45654  lptre2pt  45655  stoweidlem14  46029  stoweidlem35  46050  stoweidlem39  46054  stoweidlem50  46065  stoweidlem56  46071  stoweidlem59  46074  stoweidlem60  46075  fourier2  46242  qndenserrnbllem  46309  qndenserrn  46314  ovncvrrp  46579  ovnsubaddlem2  46586  hoidmvval0b  46605  hoiqssbllem3  46639  ormklocald  46889  natlocalincr  46891  tworepnotupword  46901  funressnfv  47055  imasetpreimafvbijlemfv1  47390  fundcmpsurinjpreimafv  47395  elsprel  47462  isubgredg  47852  isubgr3stgr  47942  grilcbri2  47971  clnbgr3stgrgrlic  47979  subthinc  49092