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  2536  moim  2545  mo4  2567  reximdv2  3148  cgsexg  3487  spcimdv  3549  spcegv  3553  euind  3684  sbcimdv  3811  reupick  4283  reximdva0  4309  uniss  4873  dfiun2g  4987  sepexlem  5246  eusvnfb  5340  reusv2lem3  5347  axprlem1  5370  axprlem2  5371  axprlem4  5373  axpr  5374  axprlem3OLD  5375  axprOLD  5378  axprglem  5382  exexneq  5391  relopabi  5779  coss1  5812  coss2  5813  ssrelrn  5851  dmss  5859  dmcosseq  5935  dmcosseqOLD  5936  dmcosseqOLDOLD  5937  funssres  6544  brprcneu  6832  brprcneuALT  6833  fv3  6860  fvelima2  6894  dffv2  6937  fvn0ssdmfun  7028  dffo4  7057  dffo5  7058  funopsn  7103  fvclss  7197  fsnex  7239  f1prex  7240  f1eqcocnv  7257  mapsnd  8836  en2  9192  en4  9194  marypha2  9354  brwdom3  9499  elirrv  9514  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  11308  xrsupsslem  13234  xrinfmsslem  13235  ishashinf  14398  hash3tpde  14428  coss12d  14907  supcvg  15791  vdwlem2  16922  ram0  16962  mreexexlem2d  17580  initoeu1  17947  termoeu1  17954  acsmapd  18489  acsmap2d  18490  dirge  18538  odcau  19545  ablfac2  20032  lspprat  21120  cmpsub  23356  cmpcld  23358  2ndcsep  23415  1stcelcls  23417  txcn  23582  fgcl  23834  ufildom1  23882  metustexhalf  24512  bcthlem5  25296  mbfi1flim  25692  itg2seq  25711  dchrisumlem3  27470  upgrex  29177  uhgrvd00  29620  wlkiswwlksupgr2  29962  wlklnwwlkln2lem  29967  usgrwwlks2on  30043  umgrwwlks2on  30044  wpthswwlks2on  30049  frcond3  30356  frgrncvvdeqlem9  30394  ubthlem1  30958  axhcompl-zf  31086  isch3  31329  cnlnssadj  32168  ac6mapd  32713  acunirnmpt  32749  f1ocnt  32891  wrdpmtrlast  33187  qsxpid  33455  zarclsint  34050  insiga  34315  bnj605  35083  bnj607  35092  bnj1018g  35139  bnj1018  35140  axprALT2  35287  cusgredgex  35338  loop1cycl  35353  erdsze2lem1  35419  fundmpss  35983  regsfromregtr  36690  bj-zfauscl  37172  bj-axseprep  37322  bj-restn0  37343  dissneqlem  37595  relowlpssretop  37619  pibt2  37672  wl-isseteq  37760  poimirlem30  37901  fdc1  37997  prdstotbnd  38045  cossss  38766  prter2  39257  lsat0cv  39409  pmapglb2N  40147  elpaddn0  40176  cdlemftr3  40941  dibglbN  41542  dihglbcpreN  41676  dihjatcclem4  41797  sticksstones3  42518  sticksstones20  42536  sn-axprlem3  42590  eu6w  43034  dfac11  43419  neik0pk1imk0  44403  rr-spce  44560  cpcolld  44614  ismnushort  44657  ax6e2ndeq  44915  ssclaxsep  45338  fnchoice  45389  rfcnnnub  45396  eliin2f  45463  founiiun0  45549  disjinfi  45551  axccd  45587  axccd2  45588  fzisoeu  45662  islpcn  45997  lptre2pt  45998  stoweidlem14  46372  stoweidlem35  46393  stoweidlem39  46397  stoweidlem50  46408  stoweidlem56  46414  stoweidlem59  46417  stoweidlem60  46418  fourier2  46585  qndenserrnbllem  46652  qndenserrn  46657  ovncvrrp  46922  ovnsubaddlem2  46929  hoidmvval0b  46948  hoiqssbllem3  46982  ormklocald  47232  natlocalincr  47234  funressnfv  47403  imasetpreimafvbijlemfv1  47763  fundcmpsurinjpreimafv  47768  elsprel  47835  isubgredg  48226  isubgr3stgr  48335  grlimedgclnbgr  48355  grlimprclnbgredg  48357  grlimpredg  48358  grlimprclnbgrvtx  48359  grilcbri2  48371  clnbgr3stgrgrlic  48380  subthinc  49802