Theorem eximdv 1946

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939

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

This theorem is used by:  2eximdv  1948  exlimdv  1962  19.41v  1978  equvinva  2059  dfmoeu  2562  moim  2571  mo4  2593  reximdv2  3174  cgsexg  3498  spcimdv  3551  spcegv  3555  euind  3686  sbcimdv  3811  reupick  4281  reximdva0  4309  uniss  4879  dfiun2g  4993  replem  5248  sepexlem  5261  eusvnfb  5363  reusv2lem3  5370  axprlem2  5394  axprlem4  5396  axpr  5397  axprlem1OLD  5398  axprlem3OLD  5399  axprOLD  5402  axprglem  5406  exexneq  5415  relopabi  5808  coss1  5840  coss2  5841  ssrelrn  5883  dmss  5891  dmcosseq  5967  dmcosseqOLD  5968  funssres  6580  brprcneu  6871  brprcneuALT  6872  fv3  6899  fvelima2  6933  dffv2  6976  fvn0ssdmfun  7069  dffo4  7098  dffo5  7099  funopsn  7144  funopsnOLD  7145  fvclss  7239  fsnex  7281  f1prex  7282  f1eqcocnv  7299  mapsnd  8882  en2  9238  en4  9240  marypha2  9397  brwdom3  9542  elirrvOLD  9558  isinffi  9985  infpwfien  10053  infmap2  10207  cfub  10238  cflm  10239  cff1  10248  cfss  10255  isf32lem9  10351  axcc4  10429  acncc  10430  domtriomlem  10432  ac6s  10474  iundom2g  10530  winalim2  10687  grudomon  10808  nsmallnq  10968  prnmadd  10988  ltexprlem1  11027  ltexprlem3  11029  ltexprlem4  11030  reclem2pr  11039  dedekind  11379  xrsupsslem  13339  xrinfmsslem  13340  ishashinf  14507  hash3tpde  14537  coss12d  15016  supcvg  15917  vdwlem2  17048  ram0  17088  mreexexlem2d  17707  initoeu1  18074  termoeu1  18081  acsmapd  18616  acsmap2d  18617  dirge  18665  qsxpid  19249  odcau  19680  ablfac2  20167  lspprat  21288  lidlunin0  21372  cmpsub  23568  cmpcld  23570  2ndcsep  23627  1stcelcls  23629  txcn  23794  fgcl  24046  ufildom1  24094  metustexhalf  24724  bcthlem5  25498  mbfi1flim  25893  itg2seq  25912  dchrisumlem3  27666  upgrex  29453  uhgrvd00  29895  wlkiswwlksupgr2  30237  wlklnwwlkln2lem  30242  usgrwwlks2on  30318  umgrwwlks2on  30319  wpthswwlks2on  30324  frcond3  30631  frgrncvvdeqlem9  30669  ubthlem1  31233  axhcompl-zf  31361  isch3  31604  cnlnssadj  32443  ac6mapd  32979  acunirnmpt  33015  padct  33074  f1ocnt  33156  wrdpmtrlast  33422  zarclsint  34271  insiga  34536  bnj605  35304  bnj607  35313  bnj1018g  35360  bnj1018  35361  axprALT2  35512  axsepg2  35561  axsepg4  35564  axpowg2  35568  karddom  35582  kardsdom  35583  cusgredgex  35622  loop1cycl  35637  erdsze2lem1  35703  fundmpss  36267  axtco1from2  37014  regsfromregtco  37077  bj-sepg  37587  bj-axseprep  37739  bj-restn0  37760  dissneqlem  38014  relowlpssretop  38038  pibt2  38091  wl-isseteq  38179  wl-dfcleq  38188  poimirlem30  38329  fdc1  38425  prdstotbnd  38473  cossss  39192  prter2  39683  lsat0cv  39835  pmapglb2N  40573  elpaddn0  40602  cdlemftr3  41367  dibglbN  41968  dihglbcpreN  42102  dihjatcclem4  42223  sticksstones3  42943  sticksstones20  42961  sn-axprlem3  43017  eu6w  43436  dfac11  43817  neik0pk1imk0  44801  rr-spce  44956  cpcolld  44996  ismnushort  45039  ax6e2ndeq  45296  ssclaxsep  45719  fnchoice  45777  rfcnnnub  45784  eliin2f  45850  founiiun0  45936  disjinfi  45938  axccd  45972  axccd2  45973  fzisoeu  46047  islpcn  46381  lptre2pt  46382  stoweidlem14  46756  stoweidlem35  46777  stoweidlem39  46781  stoweidlem50  46792  stoweidlem56  46798  stoweidlem59  46801  stoweidlem60  46802  fourier2  46969  qndenserrnbllem  47036  qndenserrn  47041  ovncvrrp  47306  ovnsubaddlem2  47313  hoidmvval0b  47332  hoiqssbllem3  47366  ormklocald  47618  natlocalincr  47620  funressnfv  47808  imasetpreimafvbijlemfv1  48180  fundcmpsurinjpreimafv  48185  elsprel  48252  isubgredg  48659  isubgr3stgr  48768  grlimedgclnbgr  48788  grlimprclnbgredg  48790  grlimpredg  48791  grlimprclnbgrvtx  48792  grilcbri2  48804  clnbgr3stgrgrlic  48813  subthinc  50249