Theorem eximdv 1918

Description: Deduction form of Theorem 19.22 of [Margaris] p. 90, see exim 1835. See eximdh 1865 and eximd 2221 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  2533  moim  2542  mo4  2564  reximdv2  3144  cgsexg  3483  spcimdv  3545  spcegv  3549  euind  3680  sbcimdv  3807  reupick  4279  reximdva0  4305  uniss  4869  dfiun2g  4983  sepexlem  5242  eusvnfb  5336  reusv2lem3  5343  axprlem1  5366  axprlem2  5367  axprlem4  5369  axpr  5370  axprlem3OLD  5371  axprOLD  5374  exexneq  5382  relopabi  5769  coss1  5802  coss2  5803  ssrelrn  5841  dmss  5849  dmcosseq  5925  dmcosseqOLD  5926  dmcosseqOLDOLD  5927  funssres  6534  brprcneu  6822  brprcneuALT  6823  fv3  6850  fvelima2  6884  dffv2  6927  fvn0ssdmfun  7017  dffo4  7046  dffo5  7047  funopsn  7091  fvclss  7185  fsnex  7227  f1prex  7228  f1eqcocnv  7245  mapsnd  8822  en2  9178  en4  9180  marypha2  9340  brwdom3  9485  elirrv  9500  isinffi  9902  infpwfien  9970  infmap2  10125  cfub  10157  cflm  10158  cff1  10166  cfss  10173  isf32lem9  10269  axcc4  10347  acncc  10348  domtriomlem  10350  ac6s  10392  iundom2g  10448  winalim2  10605  grudomon  10726  nsmallnq  10886  prnmadd  10906  ltexprlem1  10945  ltexprlem3  10947  ltexprlem4  10948  reclem2pr  10957  dedekind  11294  xrsupsslem  13220  xrinfmsslem  13221  ishashinf  14384  hash3tpde  14414  coss12d  14893  supcvg  15777  vdwlem2  16908  ram0  16948  mreexexlem2d  17566  initoeu1  17933  termoeu1  17940  acsmapd  18475  acsmap2d  18476  dirge  18524  odcau  19531  ablfac2  20018  lspprat  21106  cmpsub  23342  cmpcld  23344  2ndcsep  23401  1stcelcls  23403  txcn  23568  fgcl  23820  ufildom1  23868  metustexhalf  24498  bcthlem5  25282  mbfi1flim  25678  itg2seq  25697  dchrisumlem3  27456  upgrex  29114  uhgrvd00  29557  wlkiswwlksupgr2  29899  wlklnwwlkln2lem  29904  usgrwwlks2on  29980  umgrwwlks2on  29981  wpthswwlks2on  29986  frcond3  30293  frgrncvvdeqlem9  30331  ubthlem1  30894  axhcompl-zf  31022  isch3  31265  cnlnssadj  32104  ac6mapd  32650  acunirnmpt  32686  f1ocnt  32829  wrdpmtrlast  33124  qsxpid  33392  zarclsint  33978  insiga  34243  bnj605  35012  bnj607  35021  bnj1018g  35068  bnj1018  35069  cusgredgex  35265  loop1cycl  35280  erdsze2lem1  35346  fundmpss  35910  bj-zfauscl  37068  bj-restn0  37234  dissneqlem  37484  relowlpssretop  37508  pibt2  37561  wl-isseteq  37649  poimirlem30  37790  fdc1  37886  prdstotbnd  37934  cossss  38627  prter2  39080  lsat0cv  39232  pmapglb2N  39970  elpaddn0  39999  cdlemftr3  40764  dibglbN  41365  dihglbcpreN  41499  dihjatcclem4  41620  sticksstones3  42341  sticksstones20  42359  sn-axprlem3  42415  eu6w  42861  dfac11  43246  neik0pk1imk0  44230  rr-spce  44387  cpcolld  44441  ismnushort  44484  ax6e2ndeq  44742  ssclaxsep  45165  fnchoice  45216  rfcnnnub  45223  eliin2f  45290  founiiun0  45376  disjinfi  45378  axccd  45415  axccd2  45416  fzisoeu  45490  islpcn  45825  lptre2pt  45826  stoweidlem14  46200  stoweidlem35  46221  stoweidlem39  46225  stoweidlem50  46236  stoweidlem56  46242  stoweidlem59  46245  stoweidlem60  46246  fourier2  46413  qndenserrnbllem  46480  qndenserrn  46485  ovncvrrp  46750  ovnsubaddlem2  46757  hoidmvval0b  46776  hoiqssbllem3  46810  ormklocald  47060  natlocalincr  47062  funressnfv  47231  imasetpreimafvbijlemfv1  47591  fundcmpsurinjpreimafv  47596  elsprel  47663  isubgredg  48054  isubgr3stgr  48163  grlimedgclnbgr  48183  grlimprclnbgredg  48185  grlimpredg  48186  grlimprclnbgrvtx  48187  grilcbri2  48199  clnbgr3stgrgrlic  48208  subthinc  49630