Theorem eximdv 1920

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

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

This theorem is referenced by:  2eximdv  1922  exlimdv  1936  19.41v  1953  equvinva  2033  dfmoeu  2536  moim  2544  mo4  2566  reximdv2  3199  cgsexg  3474  spcimdv  3532  spcegv  3536  euind  3659  sbcimdv  3790  sselOLD  3915  reupick  4252  reximdva0  4285  uniss  4847  dfiun2g  4960  eusvnfb  5316  reusv2lem3  5323  axprlem1  5346  axprlem2  5347  axprlem3  5348  axpr  5351  relopabi  5732  coss1  5764  coss2  5765  ssrelrn  5803  dmss  5811  dmcosseq  5882  funssres  6478  brprcneu  6764  brprcneuALT  6765  fv3  6792  dffv2  6863  fvn0ssdmfun  6952  dffo4  6979  dffo5  6980  funopsn  7020  fvclss  7115  fsnex  7155  f1prex  7156  f1eqcocnv  7173  f1eqcocnvOLD  7174  mapsnd  8674  enp1i  9052  en2  9053  en4  9055  marypha2  9198  brwdom3  9341  isinffi  9750  infpwfien  9818  infmap2  9974  cfub  10005  cflm  10006  cff1  10014  cfss  10021  isf32lem9  10117  axcc4  10195  acncc  10196  domtriomlem  10198  ac6s  10240  iundom2g  10296  winalim2  10452  grudomon  10573  nsmallnq  10733  prnmadd  10753  ltexprlem1  10792  ltexprlem3  10794  ltexprlem4  10795  reclem2pr  10804  dedekind  11138  xrsupsslem  13041  xrinfmsslem  13042  ishashinf  14177  coss12d  14683  supcvg  15568  vdwlem2  16683  ram0  16723  mreexexlem2d  17354  initoeu1  17726  termoeu1  17733  acsmapd  18272  acsmap2d  18273  dirge  18321  odcau  19209  ablfac2  19692  lspprat  20415  cmpsub  22551  cmpcld  22553  2ndcsep  22610  1stcelcls  22612  txcn  22777  fgcl  23029  ufildom1  23077  metustexhalf  23712  bcthlem5  24492  mbfi1flim  24888  itg2seq  24907  dchrisumlem3  26639  upgrex  27462  uhgrvd00  27901  wlkiswwlksupgr2  28242  wlklnwwlkln2lem  28247  umgrwwlks2on  28322  wpthswwlks2on  28326  frcond3  28633  frgrncvvdeqlem9  28671  ubthlem1  29232  axhcompl-zf  29360  isch3  29603  cnlnssadj  30442  acunirnmpt  30996  f1ocnt  31123  qsxpid  31558  zarclsint  31822  insiga  32105  bnj605  32887  bnj607  32896  bnj1018g  32943  bnj1018  32944  cusgredgex  33083  loop1cycl  33099  erdsze2lem1  33165  fundmpss  33740  bj-zfauscl  35112  bj-restn0  35261  dissneqlem  35511  relowlpssretop  35535  pibt2  35588  poimirlem30  35807  fdc1  35904  prdstotbnd  35952  cossss  36548  prter2  36895  lsat0cv  37047  pmapglb2N  37785  elpaddn0  37814  cdlemftr3  38579  dibglbN  39180  dihglbcpreN  39314  dihjatcclem4  39435  mapdordlem2  39651  sticksstones3  40104  sticksstones20  40122  sn-axprlem3  40186  sn-dtru  40188  dfac11  40887  neik0pk1imk0  41657  rr-spce  41815  cpcolld  41876  ismnushort  41919  ax6e2ndeq  42179  fnchoice  42572  rfcnnnub  42579  eliin2f  42654  founiiun0  42728  disjinfi  42731  axccd  42768  axccd2  42769  fvelima2  42806  fzisoeu  42839  islpcn  43180  lptre2pt  43181  stoweidlem14  43555  stoweidlem35  43576  stoweidlem39  43580  stoweidlem50  43591  stoweidlem56  43597  stoweidlem59  43600  stoweidlem60  43601  fourier2  43768  qndenserrnbllem  43835  qndenserrn  43840  ovncvrrp  44102  ovnsubaddlem2  44109  hoidmvval0b  44128  hoiqssbllem3  44162  funressnfv  44537  imasetpreimafvbijlemfv1  44855  fundcmpsurinjpreimafv  44860  elsprel  44927  subthinc  46321  natlocalincr  46511  tworepnotupword  46521