Theorem eximdv 1952

Description: Deduction form of Theorem 19.22 of [Margaris] p. 90, see exim 1867. See eximdh 1897 and eximd 2256 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 1945	. 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 1945

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

This theorem is used by:  2eximdv  1954  exlimdv  1968  19.41v  1984  equvinva  2065  dfmoeu  2563  moim  2572  mo4  2594  reximdv2  3176  cgsexg  3498  spcimdv  3551  spcegv  3555  euind  3685  sbcimdv  3810  reupick  4277  reximdva0  4306  uniss  4880  dfiun2g  4993  replem  5247  sepexlem  5260  eusvnfb  5362  reusv2lem3  5369  axprlem2  5393  axprlem4  5395  axpr  5396  axprlem1OLD  5397  axprglem  5401  exexneq  5410  relopabi  5809  relopabiOLD  5810  coss1  5843  coss2  5844  ssrelrn  5888  dmss  5896  dmcosseq  5972  dmcosseqOLD  5973  funssres  6612  brprcneu  6906  brprcneuALT  6907  fv3  6934  fvelima2  6968  dffv2  7011  fvn0ssdmfun  7106  dffo4  7135  dffo5  7136  funopsn  7183  funopsnOLD  7184  fvclss  7276  fsnex  7322  f1prex  7323  f1eqcocnv  7340  mapsnd  8952  en2  9309  en4  9311  marypha2  9468  brwdom3  9613  elirrvOLD  9629  isinffi  10112  infpwfien  10180  infmap2  10334  cfub  10365  cflm  10366  cff1  10375  cfss  10382  isf32lem9  10478  axcc4  10556  acncc  10557  domtriomlem  10559  ac6s  10601  iundom2g  10663  winalim2  10820  grudomon  10941  nsmallnq  11101  prnmadd  11121  ltexprlem1  11160  ltexprlem3  11162  ltexprlem4  11163  reclem2pr  11172  dedekind  11512  xrsupsslem  13477  xrinfmsslem  13478  ishashinf  14649  hash3tpde  14679  coss12dOLD  15168  supcvg  16069  vdwlem2  17204  ram0  17244  mreexexlem2d  17869  initoeu1  18236  termoeu1  18243  acsmapd  18778  acsmap2d  18779  dirge  18827  qsxpid  19437  odcau  19869  ablfac2  20356  lspprat  21482  lidlunin0  21566  cmpsub  23773  cmpcld  23775  2ndcsep  23833  1stcelcls  23835  txcn  24000  fgcl  24252  ufildom1  24300  metustexhalf  24930  bcthlem5  25704  mbfi1flim  26099  itg2seq  26118  dchrisumlem3  27875  upgrex  29727  uhgrvd00  30172  wlkiswwlksupgr2  30523  wlklnwwlkln2lem  30528  usgrwwlks2on  30604  umgrwwlks2on  30605  wpthswwlks2on  30610  loop1cycl  30801  frcond3  30927  frgrncvvdeqlem9  30965  ubthlem1  31529  axhcompl-zf  31657  isch3  31900  cnlnssadj  32739  ac6mapd  33315  acunirnmpt  33351  padct  33407  f1ocnt  33488  wrdpmtrlast  33753  zarclsint  34615  insiga  34881  bnj605  35648  bnj607  35657  bnj1018g  35704  bnj1018  35705  axprALT2  35857  dfac15  35886  acwer1prclem  35892  acwer1prc  35893  axsepg2  35949  axsepg4  35952  axpowg2  35956  karddom  35970  kardsdom  35971  cusgredgex  36104  erdsze2lem1  36176  ptpconn  36206  mirimanoffr  36668  fundmpss  36747  axtco1from2  37478  regsfromregtco  37541  bj-sepg  38051  bj-axseprep  38260  bj-restn0  38281  dissneqlem  38531  relowlpssretop  38555  pibt2  38608  wl-isseteq  38696  wl-dfcleq  38705  poimirlem30  38836  fdc1  38946  prdstotbnd  38994  cossss  39713  prter2  40204  lsat0cv  40356  pmapglb2N  41094  elpaddn0  41123  cdlemftr3  41888  dibglbN  42489  dihglbcpreN  42623  dihjatcclem4  42744  sticksstones3  43464  sticksstones20  43482  cbvex2ivw  43529  sn-axprlem3  43539  eu6w  43953  dfac11  44330  neik0pk1imk0  45308  rr-spce  45463  cpcolld  45503  ismnushort  45546  ax6e2ndeq  45802  ssclaxsep  46236  fnchoice  46320  rfcnnnub  46327  eliin2f  46392  founiiun0  46478  disjinfi  46480  axccd  46514  axccd2  46515  fzisoeu  46589  islpcn  46922  lptre2pt  46923  stoweidlem14  47297  stoweidlem35  47318  stoweidlem39  47322  stoweidlem50  47333  stoweidlem56  47339  stoweidlem59  47342  stoweidlem60  47343  fourier2  47510  qndenserrnbllem  47577  qndenserrn  47582  ovncvrrp  47847  ovnsubaddlem2  47854  hoidmvval0b  47873  hoiqssbllem3  47907  ormklocald  48159  tmachlem-exagreecover  48229  funressnfv  48386  imasetpreimafvbijlemfv1  48758  fundcmpsurinjpreimafv  48763  elsprel  48830  isubgredg  49237  isubgr3stgr  49346  grlimedgclnbgr  49366  grlimprclnbgredg  49368  grlimpredg  49369  grlimprclnbgrvtx  49370  grilcbri2  49382  clnbgr3stgrgrlic  49391  subthinc  50909