Theorem eximdv 1918

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

Syntax hints:   → wi 4  ∃wex 1780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

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

This theorem is referenced by:  2eximdv  1920  exlimdv  1934  19.41v  1950  equvinva  2031  dfmoeu  2535  moim  2544  mo4  2566  reximdv2  3146  cgsexg  3485  spcimdv  3547  spcegv  3551  euind  3682  sbcimdv  3809  reupick  4281  reximdva0  4307  uniss  4871  dfiun2g  4985  sepexlem  5244  eusvnfb  5338  reusv2lem3  5345  axprlem1  5368  axprlem2  5369  axprlem4  5371  axpr  5372  axprlem3OLD  5373  axprOLD  5376  exexneq  5384  relopabi  5771  coss1  5804  coss2  5805  ssrelrn  5843  dmss  5851  dmcosseq  5927  dmcosseqOLD  5928  dmcosseqOLDOLD  5929  funssres  6536  brprcneu  6824  brprcneuALT  6825  fv3  6852  fvelima2  6886  dffv2  6929  fvn0ssdmfun  7019  dffo4  7048  dffo5  7049  funopsn  7093  fvclss  7187  fsnex  7229  f1prex  7230  f1eqcocnv  7247  mapsnd  8824  en2  9180  en4  9182  marypha2  9342  brwdom3  9487  elirrv  9502  isinffi  9904  infpwfien  9972  infmap2  10127  cfub  10159  cflm  10160  cff1  10168  cfss  10175  isf32lem9  10271  axcc4  10349  acncc  10350  domtriomlem  10352  ac6s  10394  iundom2g  10450  winalim2  10607  grudomon  10728  nsmallnq  10888  prnmadd  10908  ltexprlem1  10947  ltexprlem3  10949  ltexprlem4  10950  reclem2pr  10959  dedekind  11296  xrsupsslem  13222  xrinfmsslem  13223  ishashinf  14386  hash3tpde  14416  coss12d  14895  supcvg  15779  vdwlem2  16910  ram0  16950  mreexexlem2d  17568  initoeu1  17935  termoeu1  17942  acsmapd  18477  acsmap2d  18478  dirge  18526  odcau  19533  ablfac2  20020  lspprat  21108  cmpsub  23344  cmpcld  23346  2ndcsep  23403  1stcelcls  23405  txcn  23570  fgcl  23822  ufildom1  23870  metustexhalf  24500  bcthlem5  25284  mbfi1flim  25680  itg2seq  25699  dchrisumlem3  27458  upgrex  29165  uhgrvd00  29608  wlkiswwlksupgr2  29950  wlklnwwlkln2lem  29955  usgrwwlks2on  30031  umgrwwlks2on  30032  wpthswwlks2on  30037  frcond3  30344  frgrncvvdeqlem9  30382  ubthlem1  30945  axhcompl-zf  31073  isch3  31316  cnlnssadj  32155  ac6mapd  32701  acunirnmpt  32737  f1ocnt  32880  wrdpmtrlast  33175  qsxpid  33443  zarclsint  34029  insiga  34294  bnj605  35063  bnj607  35072  bnj1018g  35119  bnj1018  35120  cusgredgex  35316  loop1cycl  35331  erdsze2lem1  35397  fundmpss  35961  regsfromregtr  36668  bj-zfauscl  37125  bj-restn0  37295  dissneqlem  37545  relowlpssretop  37569  pibt2  37622  wl-isseteq  37710  poimirlem30  37851  fdc1  37947  prdstotbnd  37995  cossss  38698  prter2  39151  lsat0cv  39303  pmapglb2N  40041  elpaddn0  40070  cdlemftr3  40835  dibglbN  41436  dihglbcpreN  41570  dihjatcclem4  41691  sticksstones3  42412  sticksstones20  42430  sn-axprlem3  42484  eu6w  42929  dfac11  43314  neik0pk1imk0  44298  rr-spce  44455  cpcolld  44509  ismnushort  44552  ax6e2ndeq  44810  ssclaxsep  45233  fnchoice  45284  rfcnnnub  45291  eliin2f  45358  founiiun0  45444  disjinfi  45446  axccd  45483  axccd2  45484  fzisoeu  45558  islpcn  45893  lptre2pt  45894  stoweidlem14  46268  stoweidlem35  46289  stoweidlem39  46293  stoweidlem50  46304  stoweidlem56  46310  stoweidlem59  46313  stoweidlem60  46314  fourier2  46481  qndenserrnbllem  46548  qndenserrn  46553  ovncvrrp  46818  ovnsubaddlem2  46825  hoidmvval0b  46844  hoiqssbllem3  46878  ormklocald  47128  natlocalincr  47130  funressnfv  47299  imasetpreimafvbijlemfv1  47659  fundcmpsurinjpreimafv  47664  elsprel  47731  isubgredg  48122  isubgr3stgr  48231  grlimedgclnbgr  48251  grlimprclnbgredg  48253  grlimpredg  48254  grlimprclnbgrvtx  48255  grilcbri2  48267  clnbgr3stgrgrlic  48276  subthinc  49698