Theorem eximdv 1921

Description: Deduction form of Theorem 19.22 of [Margaris] p. 90, see exim 1837. See eximdh 1868 and eximd 2210 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 1782

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

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

This theorem is referenced by:  2eximdv  1923  exlimdv  1937  19.41v  1954  equvinva  2034  dfmoeu  2531  moim  2539  mo4  2561  reximdv2  3165  cgsexg  3519  spcimdv  3584  spcegv  3588  euind  3721  sbcimdv  3852  sselOLD  3977  reupick  4319  reximdva0  4352  uniss  4917  dfiun2g  5034  eusvnfb  5392  reusv2lem3  5399  axprlem1  5422  axprlem2  5423  axprlem3  5424  axpr  5427  exexneq  5435  relopabi  5823  coss1  5856  coss2  5857  ssrelrn  5895  dmss  5903  dmcosseq  5973  funssres  6593  brprcneu  6882  brprcneuALT  6883  fv3  6910  dffv2  6987  fvn0ssdmfun  7077  dffo4  7105  dffo5  7106  funopsn  7146  fvclss  7241  fsnex  7281  f1prex  7282  f1eqcocnv  7299  f1eqcocnvOLD  7300  mapsnd  8880  enp1iOLD  9280  en2  9281  en4  9283  marypha2  9434  brwdom3  9577  isinffi  9987  infpwfien  10057  infmap2  10213  cfub  10244  cflm  10245  cff1  10253  cfss  10260  isf32lem9  10356  axcc4  10434  acncc  10435  domtriomlem  10437  ac6s  10479  iundom2g  10535  winalim2  10691  grudomon  10812  nsmallnq  10972  prnmadd  10992  ltexprlem1  11031  ltexprlem3  11033  ltexprlem4  11034  reclem2pr  11043  dedekind  11377  xrsupsslem  13286  xrinfmsslem  13287  ishashinf  14424  coss12d  14919  supcvg  15802  vdwlem2  16915  ram0  16955  mreexexlem2d  17589  initoeu1  17961  termoeu1  17968  acsmapd  18507  acsmap2d  18508  dirge  18556  odcau  19472  ablfac2  19959  lspprat  20766  cmpsub  22904  cmpcld  22906  2ndcsep  22963  1stcelcls  22965  txcn  23130  fgcl  23382  ufildom1  23430  metustexhalf  24065  bcthlem5  24845  mbfi1flim  25241  itg2seq  25260  dchrisumlem3  26994  upgrex  28352  uhgrvd00  28791  wlkiswwlksupgr2  29131  wlklnwwlkln2lem  29136  umgrwwlks2on  29211  wpthswwlks2on  29215  frcond3  29522  frgrncvvdeqlem9  29560  ubthlem1  30123  axhcompl-zf  30251  isch3  30494  cnlnssadj  31333  acunirnmpt  31884  f1ocnt  32013  qsxpid  32474  zarclsint  32852  insiga  33135  bnj605  33918  bnj607  33927  bnj1018g  33974  bnj1018  33975  cusgredgex  34112  loop1cycl  34128  erdsze2lem1  34194  fundmpss  34738  bj-zfauscl  35804  bj-restn0  35971  dissneqlem  36221  relowlpssretop  36245  pibt2  36298  poimirlem30  36518  fdc1  36614  prdstotbnd  36662  cossss  37295  prter2  37751  lsat0cv  37903  pmapglb2N  38642  elpaddn0  38671  cdlemftr3  39436  dibglbN  40037  dihglbcpreN  40171  dihjatcclem4  40292  mapdordlem2  40508  sticksstones3  40964  sticksstones20  40982  sn-axprlem3  41034  dfac11  41804  neik0pk1imk0  42798  rr-spce  42956  cpcolld  43017  ismnushort  43060  ax6e2ndeq  43320  fnchoice  43713  rfcnnnub  43720  eliin2f  43793  founiiun0  43888  disjinfi  43891  axccd  43928  axccd2  43929  fvelima2  43964  fzisoeu  44010  islpcn  44355  lptre2pt  44356  stoweidlem14  44730  stoweidlem35  44751  stoweidlem39  44755  stoweidlem50  44766  stoweidlem56  44772  stoweidlem59  44775  stoweidlem60  44776  fourier2  44943  qndenserrnbllem  45010  qndenserrn  45015  ovncvrrp  45280  ovnsubaddlem2  45287  hoidmvval0b  45306  hoiqssbllem3  45340  natlocalincr  45590  tworepnotupword  45600  funressnfv  45753  imasetpreimafvbijlemfv1  46071  fundcmpsurinjpreimafv  46076  elsprel  46143  subthinc  47660