Theorem eximdv 2018

Description: Deduction form of Theorem 19.22 of [Margaris] p. 90, see exim 1934. (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 2011	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		alimdv.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	eximdh 1967	1 ⊢ (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))

Syntax hints:   → wi 4  ∃wex 1880

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

This theorem depends on definitions:  df-bi 199  df-ex 1881

This theorem is referenced by:  2eximdv  2020  exlimdv  2034  19.41v  2050  19.41vOLD  2102  equvinvOLD  2137  equvinva  2138  moim  2610  dfmo  2668  reximdv2  3222  cgsexg  3455  spc3egv  3514  euind  3618  ssel  3821  reupick  4140  reximdva0  4162  uniss  4681  eusvnfb  5093  reusv2lem3  5100  relopabi  5478  coss1  5510  coss2  5511  ssrelrn  5547  dmss  5555  dmcosseq  5620  funssres  6166  brprcneu  6425  fv3  6451  dffv2  6518  fvn0ssdmfun  6599  dffo4  6624  dffo5  6625  funopsn  6664  fvclss  6755  fsnex  6793  f1prex  6794  f1eqcocnv  6811  mapsnd  8164  enp1i  8464  en2  8465  en4  8467  marypha2  8614  brwdom3  8756  isinffi  9131  infpwfien  9198  infmap2  9355  cfub  9386  cflm  9387  cff1  9395  cfss  9402  isf32lem9  9498  axcc4  9576  acncc  9577  domtriomlem  9579  ac6s  9621  iundom2g  9677  winalim2  9833  grudomon  9954  nsmallnq  10114  prnmadd  10134  ltexprlem1  10173  ltexprlem3  10175  ltexprlem4  10176  reclem2pr  10185  dedekind  10519  xrsupsslem  12425  xrinfmsslem  12426  ishashinf  13536  coss12d  14090  supcvg  14962  vdwlem2  16057  ram0  16097  mreexexlem2d  16658  initoeu1  17013  termoeu1  17020  acsmapd  17531  acsmap2d  17532  dirge  17590  odcau  18370  ablfac2  18842  lspprat  19514  cmpsub  21574  cmpcld  21576  2ndcsep  21633  1stcelcls  21635  txcn  21800  fgcl  22052  ufildom1  22100  metustexhalf  22731  bcthlem5  23496  mbfi1flim  23889  itg2seq  23908  dchrisumlem3  25593  upgrex  26390  uhgrvd00  26832  wlkiswwlksupgr2  27176  wlklnwwlkln2lem  27182  umgrwwlks2on  27286  wpthswwlks2on  27290  frcond3  27650  frgrncvvdeqlem9  27688  ubthlem1  28281  axhcompl-zf  28410  isch3  28653  cnlnssadj  29494  acunirnmpt  30008  f1ocnt  30106  insiga  30745  bnj605  31523  bnj607  31532  bnj1018  31578  erdsze2lem1  31731  fundmpss  32206  bj-zfauscl  33445  bj-restn0  33566  dissneqlem  33733  relowlpssretop  33757  poimirlem30  33983  fdc1  34084  prdstotbnd  34135  cossss  34728  prter2  34956  lsat0cv  35108  pmapglb2N  35846  elpaddn0  35875  cdlemftr3  36640  dibglbN  37241  dihglbcpreN  37375  dihjatcclem4  37496  mapdordlem2  37712  dfac11  38475  neik0pk1imk0  39185  ax6e2ndeq  39603  fnchoice  40006  rfcnnnub  40013  eliin2f  40102  founiiun0  40185  axccd  40231  axccd2  40232  fvelima2  40275  fzisoeu  40312  islpcn  40666  lptre2pt  40667  stoweidlem14  41025  stoweidlem35  41046  stoweidlem39  41050  stoweidlem50  41061  stoweidlem56  41067  stoweidlem59  41070  stoweidlem60  41071  fourier2  41238  qndenserrnbllem  41305  qndenserrn  41310  ovncvrrp  41572  ovnsubaddlem2  41579  hoidmvval0b  41598  hoiqssbllem3  41632  funressnfv  41974  elsprel  42572