Theorem eximdv 1950

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

This proof depends on syntax axioms:   → wi 4  ∃wex 1812

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-ex 1813

This theorem is used by:  2eximdv  1952  exlimdv  1966  19.41v  1982  equvinva  2063  dfmoeu  2561  moim  2570  mo4  2592  reximdv2  3173  cgsexg  3495  spcimdv  3548  spcegv  3552  euind  3682  sbcimdv  3807  reupick  4275  reximdva0  4303  uniss  4875  dfiun2g  4988  replem  5241  sepexlem  5254  eusvnfb  5355  reusv2lem3  5362  axprlem2  5386  axprlem4  5388  axpr  5389  axprlem1OLD  5390  axprglem  5394  exexneq  5403  relopabi  5800  coss1  5833  coss2  5834  ssrelrn  5876  dmss  5884  dmcosseq  5960  dmcosseqOLD  5961  funssres  6584  brprcneu  6875  brprcneuALT  6876  fv3  6903  fvelima2  6937  dffv2  6980  fvn0ssdmfun  7074  dffo4  7103  dffo5  7104  funopsn  7151  funopsnOLD  7152  fvclss  7245  fsnex  7291  f1prex  7292  f1eqcocnv  7309  mapsnd  8914  en2  9271  en4  9273  marypha2  9431  brwdom3  9576  elirrvOLD  9592  isinffi  10073  infpwfien  10141  infmap2  10295  cfub  10326  cflm  10327  cff1  10336  cfss  10343  isf32lem9  10439  axcc4  10517  acncc  10518  domtriomlem  10520  ac6s  10562  iundom2g  10624  winalim2  10781  grudomon  10902  nsmallnq  11062  prnmadd  11082  ltexprlem1  11121  ltexprlem3  11123  ltexprlem4  11124  reclem2pr  11133  dedekind  11473  xrsupsslem  13437  xrinfmsslem  13438  ishashinf  14608  hash3tpde  14638  coss12d  15125  supcvg  16025  vdwlem2  17160  ram0  17200  mreexexlem2d  17819  initoeu1  18186  termoeu1  18193  acsmapd  18728  acsmap2d  18729  dirge  18777  qsxpid  19387  odcau  19818  ablfac2  20305  lspprat  21431  lidlunin0  21515  cmpsub  23718  cmpcld  23720  2ndcsep  23778  1stcelcls  23780  txcn  23945  fgcl  24197  ufildom1  24245  metustexhalf  24875  bcthlem5  25649  mbfi1flim  26044  itg2seq  26063  dchrisumlem3  27818  upgrex  29670  uhgrvd00  30115  wlkiswwlksupgr2  30466  wlklnwwlkln2lem  30471  usgrwwlks2on  30547  umgrwwlks2on  30548  wpthswwlks2on  30553  loop1cycl  30744  frcond3  30870  frgrncvvdeqlem9  30908  ubthlem1  31472  axhcompl-zf  31600  isch3  31843  cnlnssadj  32682  ac6mapd  33217  acunirnmpt  33253  padct  33310  f1ocnt  33392  wrdpmtrlast  33654  zarclsint  34504  insiga  34770  bnj605  35537  bnj607  35546  bnj1018g  35593  bnj1018  35594  axprALT2  35734  acwer1prclem  35759  acwer1prc  35760  axsepg2  35808  axsepg4  35811  axpowg2  35815  karddom  35829  kardsdom  35830  cusgredgex  35906  erdsze2lem1  35968  fundmpss  36532  axtco1from2  37263  regsfromregtco  37326  bj-sepg  37836  bj-axseprep  37990  bj-restn0  38011  dissneqlem  38263  relowlpssretop  38287  pibt2  38340  wl-isseteq  38428  wl-dfcleq  38437  poimirlem30  38568  fdc1  38680  prdstotbnd  38728  cossss  39447  prter2  39938  lsat0cv  40090  pmapglb2N  40828  elpaddn0  40857  cdlemftr3  41622  dibglbN  42223  dihglbcpreN  42357  dihjatcclem4  42478  sticksstones3  43198  sticksstones20  43216  sn-axprlem3  43272  eu6w  43687  dfac11  44063  neik0pk1imk0  45046  rr-spce  45201  cpcolld  45241  ismnushort  45284  ax6e2ndeq  45541  ssclaxsep  45971  fnchoice  46045  rfcnnnub  46052  eliin2f  46118  founiiun0  46204  disjinfi  46206  axccd  46240  axccd2  46241  fzisoeu  46315  islpcn  46648  lptre2pt  46649  stoweidlem14  47023  stoweidlem35  47044  stoweidlem39  47048  stoweidlem50  47059  stoweidlem56  47065  stoweidlem59  47068  stoweidlem60  47069  fourier2  47236  qndenserrnbllem  47303  qndenserrn  47308  ovncvrrp  47573  ovnsubaddlem2  47580  hoidmvval0b  47599  hoiqssbllem3  47633  ormklocald  47885  tmachlem-exagreecover  47955  funressnfv  48112  imasetpreimafvbijlemfv1  48484  fundcmpsurinjpreimafv  48489  elsprel  48556  isubgredg  48963  isubgr3stgr  49072  grlimedgclnbgr  49092  grlimprclnbgredg  49094  grlimpredg  49095  grlimprclnbgrvtx  49096  grilcbri2  49108  clnbgr3stgrgrlic  49117  subthinc  50550