Theorem eximdv 1914

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

Syntax hints:   → wi 4  ∃wex 1775

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907

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

This theorem is referenced by:  2eximdv  1916  exlimdv  1930  19.41v  1946  equvinva  2026  dfmoeu  2533  moim  2541  mo4  2563  reximdv2  3161  cgsexg  3523  spcimdv  3592  spcegv  3596  euind  3732  sbcimdv  3864  reupick  4334  reximdva0  4360  uniss  4919  dfiun2g  5034  sepexlem  5304  eusvnfb  5398  reusv2lem3  5405  axprlem1  5428  axprlem2  5429  axprlem4  5431  axpr  5432  axprlem3OLD  5433  axprOLD  5436  exexneq  5444  relopabi  5834  coss1  5868  coss2  5869  ssrelrn  5907  dmss  5915  dmcosseq  5989  dmcosseqOLD  5990  funssres  6611  brprcneu  6896  brprcneuALT  6897  fv3  6924  dffv2  7003  fvn0ssdmfun  7093  dffo4  7122  dffo5  7123  funopsn  7167  fvclss  7260  fsnex  7302  f1prex  7303  f1eqcocnv  7320  mapsnd  8924  enp1iOLD  9311  en2  9312  en4  9314  marypha2  9476  brwdom3  9619  isinffi  10029  infpwfien  10099  infmap2  10254  cfub  10286  cflm  10287  cff1  10295  cfss  10302  isf32lem9  10398  axcc4  10476  acncc  10477  domtriomlem  10479  ac6s  10521  iundom2g  10577  winalim2  10733  grudomon  10854  nsmallnq  11014  prnmadd  11034  ltexprlem1  11073  ltexprlem3  11075  ltexprlem4  11076  reclem2pr  11085  dedekind  11421  xrsupsslem  13345  xrinfmsslem  13346  ishashinf  14498  hash3tpde  14528  coss12d  15007  supcvg  15888  vdwlem2  17015  ram0  17055  mreexexlem2d  17689  initoeu1  18064  termoeu1  18071  acsmapd  18611  acsmap2d  18612  dirge  18660  odcau  19636  ablfac2  20123  lspprat  21172  cmpsub  23423  cmpcld  23425  2ndcsep  23482  1stcelcls  23484  txcn  23649  fgcl  23901  ufildom1  23949  metustexhalf  24584  bcthlem5  25375  mbfi1flim  25772  itg2seq  25791  dchrisumlem3  27549  upgrex  29123  uhgrvd00  29566  wlkiswwlksupgr2  29906  wlklnwwlkln2lem  29911  umgrwwlks2on  29986  wpthswwlks2on  29990  frcond3  30297  frgrncvvdeqlem9  30335  ubthlem1  30898  axhcompl-zf  31026  isch3  31269  cnlnssadj  32108  acunirnmpt  32675  f1ocnt  32809  wrdpmtrlast  33095  qsxpid  33369  zarclsint  33832  insiga  34117  bnj605  34899  bnj607  34908  bnj1018g  34955  bnj1018  34956  cusgredgex  35105  loop1cycl  35121  erdsze2lem1  35187  fundmpss  35747  bj-zfauscl  36906  bj-restn0  37072  dissneqlem  37322  relowlpssretop  37346  pibt2  37399  wl-isseteq  37485  poimirlem30  37636  fdc1  37732  prdstotbnd  37780  cossss  38406  prter2  38862  lsat0cv  39014  pmapglb2N  39753  elpaddn0  39782  cdlemftr3  40547  dibglbN  41148  dihglbcpreN  41282  dihjatcclem4  41403  mapdordlem2  41619  sticksstones3  42129  sticksstones20  42147  sn-axprlem3  42234  eu6w  42662  dfac11  43050  neik0pk1imk0  44036  rr-spce  44193  cpcolld  44253  ismnushort  44296  ax6e2ndeq  44556  ssclaxsep  44946  fnchoice  44966  rfcnnnub  44973  eliin2f  45043  founiiun0  45132  disjinfi  45134  axccd  45171  axccd2  45172  fvelima2  45204  fzisoeu  45250  islpcn  45594  lptre2pt  45595  stoweidlem14  45969  stoweidlem35  45990  stoweidlem39  45994  stoweidlem50  46005  stoweidlem56  46011  stoweidlem59  46014  stoweidlem60  46015  fourier2  46182  qndenserrnbllem  46249  qndenserrn  46254  ovncvrrp  46519  ovnsubaddlem2  46526  hoidmvval0b  46545  hoiqssbllem3  46579  natlocalincr  46829  tworepnotupword  46839  funressnfv  46992  imasetpreimafvbijlemfv1  47327  fundcmpsurinjpreimafv  47332  elsprel  47399  isubgredg  47789  isubgr3stgr  47877  grilcbri2  47906  clnbgr3stgrgrlic  47914  subthinc  48839