Theorem eximdv 1950

Description: Deduction form of Theorem 19.22 of [Margaris] p. 90, see exim 1867. See eximdh 1897 and eximd 2255 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  2565  moim  2574  mo4  2596  reximdv2  3177  cgsexg  3501  spcimdv  3554  spcegv  3558  euind  3689  sbcimdv  3814  reupick  4282  reximdva0  4310  uniss  4882  dfiun2g  4996  replem  5251  sepexlem  5264  eusvnfb  5366  reusv2lem3  5373  axprlem2  5397  axprlem4  5399  axpr  5400  axprlem1OLD  5401  axprlem3OLD  5402  axprOLD  5405  axprglem  5409  exexneq  5418  relopabi  5811  coss1  5843  coss2  5844  ssrelrn  5886  dmss  5894  dmcosseq  5970  dmcosseqOLD  5971  funssres  6584  brprcneu  6875  brprcneuALT  6876  fv3  6903  fvelima2  6937  dffv2  6980  fvn0ssdmfun  7073  dffo4  7102  dffo5  7103  funopsn  7150  funopsnOLD  7151  fvclss  7244  fsnex  7290  f1prex  7291  f1eqcocnv  7308  mapsnd  8890  en2  9247  en4  9249  marypha2  9406  brwdom3  9551  elirrvOLD  9567  isinffi  9994  infpwfien  10062  infmap2  10216  cfub  10247  cflm  10248  cff1  10257  cfss  10264  isf32lem9  10360  axcc4  10438  acncc  10439  domtriomlem  10441  ac6s  10483  iundom2g  10541  winalim2  10698  grudomon  10819  nsmallnq  10979  prnmadd  10999  ltexprlem1  11038  ltexprlem3  11040  ltexprlem4  11041  reclem2pr  11050  dedekind  11390  xrsupsslem  13351  xrinfmsslem  13352  ishashinf  14520  hash3tpde  14550  coss12d  15035  supcvg  15935  vdwlem2  17066  ram0  17106  mreexexlem2d  17725  initoeu1  18092  termoeu1  18099  acsmapd  18634  acsmap2d  18635  dirge  18683  qsxpid  19289  odcau  19720  ablfac2  20207  lspprat  21329  lidlunin0  21413  cmpsub  23609  cmpcld  23611  2ndcsep  23669  1stcelcls  23671  txcn  23836  fgcl  24088  ufildom1  24136  metustexhalf  24766  bcthlem5  25540  mbfi1flim  25935  itg2seq  25954  dchrisumlem3  27708  upgrex  29499  uhgrvd00  29944  wlkiswwlksupgr2  30295  wlklnwwlkln2lem  30300  usgrwwlks2on  30376  umgrwwlks2on  30377  wpthswwlks2on  30382  loop1cycl  30573  frcond3  30693  frgrncvvdeqlem9  30731  ubthlem1  31295  axhcompl-zf  31423  isch3  31666  cnlnssadj  32505  ac6mapd  33041  acunirnmpt  33077  padct  33135  f1ocnt  33217  wrdpmtrlast  33479  zarclsint  34328  insiga  34594  bnj605  35362  bnj607  35371  bnj1018g  35418  bnj1018  35419  axprALT2  35563  axsepg2  35612  axsepg4  35615  axpowg2  35619  karddom  35633  kardsdom  35634  cusgredgex  35666  erdsze2lem1  35734  fundmpss  36298  axtco1from2  37045  regsfromregtco  37108  bj-sepg  37618  bj-axseprep  37770  bj-restn0  37791  dissneqlem  38045  relowlpssretop  38069  pibt2  38122  wl-isseteq  38210  wl-dfcleq  38219  poimirlem30  38360  fdc1  38457  prdstotbnd  38505  cossss  39224  prter2  39715  lsat0cv  39867  pmapglb2N  40605  elpaddn0  40634  cdlemftr3  41399  dibglbN  42000  dihglbcpreN  42134  dihjatcclem4  42255  sticksstones3  42975  sticksstones20  42993  sn-axprlem3  43049  eu6w  43468  dfac11  43849  neik0pk1imk0  44833  rr-spce  44988  cpcolld  45028  ismnushort  45071  ax6e2ndeq  45328  ssclaxsep  45751  fnchoice  45809  rfcnnnub  45816  eliin2f  45882  founiiun0  45968  disjinfi  45970  axccd  46004  axccd2  46005  fzisoeu  46079  islpcn  46413  lptre2pt  46414  stoweidlem14  46788  stoweidlem35  46809  stoweidlem39  46813  stoweidlem50  46824  stoweidlem56  46830  stoweidlem59  46833  stoweidlem60  46834  fourier2  47001  qndenserrnbllem  47068  qndenserrn  47073  ovncvrrp  47338  ovnsubaddlem2  47345  hoidmvval0b  47364  hoiqssbllem3  47398  ormklocald  47650  natlocalincr  47652  funressnfv  47840  imasetpreimafvbijlemfv1  48212  fundcmpsurinjpreimafv  48217  elsprel  48284  isubgredg  48691  isubgr3stgr  48800  grlimedgclnbgr  48820  grlimprclnbgredg  48822  grlimpredg  48823  grlimprclnbgrvtx  48824  grilcbri2  48836  clnbgr3stgrgrlic  48845  subthinc  50280