Theorem eximdv 1919

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

Syntax hints:   → wi 4  ∃wex 1781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207  df-ex 1782

This theorem is referenced by:  2eximdv  1921  exlimdv  1935  19.41v  1951  equvinva  2032  dfmoeu  2535  moim  2544  mo4  2566  reximdv2  3147  cgsexg  3474  spcimdv  3535  spcegv  3539  euind  3670  sbcimdv  3797  reupick  4269  reximdva0  4295  uniss  4858  dfiun2g  4972  replem  5223  sepexlem  5234  eusvnfb  5335  reusv2lem3  5342  axprlem2  5366  axprlem4  5368  axpr  5369  axprlem1OLD  5370  axprlem3OLD  5371  axprOLD  5374  axprglem  5378  exexneq  5387  relopabi  5778  coss1  5810  coss2  5811  ssrelrn  5849  dmss  5857  dmcosseq  5933  dmcosseqOLD  5934  dmcosseqOLDOLD  5935  funssres  6542  brprcneu  6830  brprcneuALT  6831  fv3  6858  fvelima2  6892  dffv2  6935  fvn0ssdmfun  7026  dffo4  7055  dffo5  7056  funopsn  7101  funopsnOLD  7102  fvclss  7196  fsnex  7238  f1prex  7239  f1eqcocnv  7256  mapsnd  8834  en2  9190  en4  9192  marypha2  9352  brwdom3  9497  elirrv  9512  isinffi  9916  infpwfien  9984  infmap2  10139  cfub  10171  cflm  10172  cff1  10180  cfss  10187  isf32lem9  10283  axcc4  10361  acncc  10362  domtriomlem  10364  ac6s  10406  iundom2g  10462  winalim2  10619  grudomon  10740  nsmallnq  10900  prnmadd  10920  ltexprlem1  10959  ltexprlem3  10961  ltexprlem4  10962  reclem2pr  10971  dedekind  11309  xrsupsslem  13259  xrinfmsslem  13260  ishashinf  14425  hash3tpde  14455  coss12d  14934  supcvg  15821  vdwlem2  16953  ram0  16993  mreexexlem2d  17611  initoeu1  17978  termoeu1  17985  acsmapd  18520  acsmap2d  18521  dirge  18569  odcau  19579  ablfac2  20066  lspprat  21151  cmpsub  23365  cmpcld  23367  2ndcsep  23424  1stcelcls  23426  txcn  23591  fgcl  23843  ufildom1  23891  metustexhalf  24521  bcthlem5  25295  mbfi1flim  25690  itg2seq  25709  dchrisumlem3  27454  upgrex  29161  uhgrvd00  29603  wlkiswwlksupgr2  29945  wlklnwwlkln2lem  29950  usgrwwlks2on  30026  umgrwwlks2on  30027  wpthswwlks2on  30032  frcond3  30339  frgrncvvdeqlem9  30377  ubthlem1  30941  axhcompl-zf  31069  isch3  31312  cnlnssadj  32151  ac6mapd  32696  acunirnmpt  32732  padct  32791  f1ocnt  32873  wrdpmtrlast  33154  qsxpid  33422  zarclsint  34016  insiga  34281  bnj605  35049  bnj607  35058  bnj1018g  35105  bnj1018  35106  axprALT2  35253  cusgredgex  35304  loop1cycl  35319  erdsze2lem1  35385  fundmpss  35949  axtco1from2  36657  regsfromregtco  36720  bj-zfauscl  37231  bj-axseprep  37381  bj-restn0  37402  dissneqlem  37656  relowlpssretop  37680  pibt2  37733  wl-isseteq  37821  wl-dfcleq  37830  poimirlem30  37971  fdc1  38067  prdstotbnd  38115  cossss  38836  prter2  39327  lsat0cv  39479  pmapglb2N  40217  elpaddn0  40246  cdlemftr3  41011  dibglbN  41612  dihglbcpreN  41746  dihjatcclem4  41867  sticksstones3  42587  sticksstones20  42605  sn-axprlem3  42659  eu6w  43109  dfac11  43490  neik0pk1imk0  44474  rr-spce  44631  cpcolld  44685  ismnushort  44728  ax6e2ndeq  44986  ssclaxsep  45409  fnchoice  45460  rfcnnnub  45467  eliin2f  45534  founiiun0  45620  disjinfi  45622  axccd  45658  axccd2  45659  fzisoeu  45733  islpcn  46067  lptre2pt  46068  stoweidlem14  46442  stoweidlem35  46463  stoweidlem39  46467  stoweidlem50  46478  stoweidlem56  46484  stoweidlem59  46487  stoweidlem60  46488  fourier2  46655  qndenserrnbllem  46722  qndenserrn  46727  ovncvrrp  46992  ovnsubaddlem2  46999  hoidmvval0b  47018  hoiqssbllem3  47052  ormklocald  47304  natlocalincr  47306  funressnfv  47491  imasetpreimafvbijlemfv1  47863  fundcmpsurinjpreimafv  47868  elsprel  47935  isubgredg  48342  isubgr3stgr  48451  grlimedgclnbgr  48471  grlimprclnbgredg  48473  grlimpredg  48474  grlimprclnbgrvtx  48475  grilcbri2  48487  clnbgr3stgrgrlic  48496  subthinc  49918