Theorem eximdv 1917

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

Syntax hints:   → wi 4  ∃wex 1779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

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

This theorem is referenced by:  2eximdv  1919  exlimdv  1933  19.41v  1949  equvinva  2030  dfmoeu  2529  moim  2537  mo4  2559  reximdv2  3139  cgsexg  3481  spcimdv  3548  spcegv  3552  euind  3684  sbcimdv  3811  reupick  4280  reximdva0  4306  uniss  4866  dfiun2g  4980  sepexlem  5238  eusvnfb  5332  reusv2lem3  5339  axprlem1  5362  axprlem2  5363  axprlem4  5365  axpr  5366  axprlem3OLD  5367  axprOLD  5370  exexneq  5378  relopabi  5765  coss1  5798  coss2  5799  ssrelrn  5837  dmss  5845  dmcosseq  5919  dmcosseqOLD  5920  dmcosseqOLDOLD  5921  funssres  6526  brprcneu  6812  brprcneuALT  6813  fv3  6840  fvelima2  6875  dffv2  6918  fvn0ssdmfun  7008  dffo4  7037  dffo5  7038  funopsn  7082  fvclss  7177  fsnex  7220  f1prex  7221  f1eqcocnv  7238  mapsnd  8813  en2  9169  en4  9171  marypha2  9329  brwdom3  9474  elirrv  9489  isinffi  9888  infpwfien  9956  infmap2  10111  cfub  10143  cflm  10144  cff1  10152  cfss  10159  isf32lem9  10255  axcc4  10333  acncc  10334  domtriomlem  10336  ac6s  10378  iundom2g  10434  winalim2  10590  grudomon  10711  nsmallnq  10871  prnmadd  10891  ltexprlem1  10930  ltexprlem3  10932  ltexprlem4  10933  reclem2pr  10942  dedekind  11279  xrsupsslem  13209  xrinfmsslem  13210  ishashinf  14370  hash3tpde  14400  coss12d  14879  supcvg  15763  vdwlem2  16894  ram0  16934  mreexexlem2d  17551  initoeu1  17918  termoeu1  17925  acsmapd  18460  acsmap2d  18461  dirge  18509  odcau  19483  ablfac2  19970  lspprat  21060  cmpsub  23285  cmpcld  23287  2ndcsep  23344  1stcelcls  23346  txcn  23511  fgcl  23763  ufildom1  23811  metustexhalf  24442  bcthlem5  25226  mbfi1flim  25622  itg2seq  25641  dchrisumlem3  27400  upgrex  29037  uhgrvd00  29480  wlkiswwlksupgr2  29822  wlklnwwlkln2lem  29827  umgrwwlks2on  29902  wpthswwlks2on  29906  frcond3  30213  frgrncvvdeqlem9  30251  ubthlem1  30814  axhcompl-zf  30942  isch3  31185  cnlnssadj  32024  ac6mapd  32567  acunirnmpt  32602  f1ocnt  32745  wrdpmtrlast  33035  qsxpid  33299  zarclsint  33839  insiga  34104  bnj605  34874  bnj607  34883  bnj1018g  34930  bnj1018  34931  cusgredgex  35099  loop1cycl  35114  erdsze2lem1  35180  fundmpss  35744  bj-zfauscl  36902  bj-restn0  37068  dissneqlem  37318  relowlpssretop  37342  pibt2  37395  wl-isseteq  37483  poimirlem30  37634  fdc1  37730  prdstotbnd  37778  cossss  38406  prter2  38864  lsat0cv  39016  pmapglb2N  39754  elpaddn0  39783  cdlemftr3  40548  dibglbN  41149  dihglbcpreN  41283  dihjatcclem4  41404  mapdordlem2  41620  sticksstones3  42125  sticksstones20  42143  sn-axprlem3  42194  eu6w  42653  dfac11  43039  neik0pk1imk0  44024  rr-spce  44181  cpcolld  44235  ismnushort  44278  ax6e2ndeq  44537  ssclaxsep  44960  fnchoice  45011  rfcnnnub  45018  eliin2f  45086  founiiun0  45172  disjinfi  45174  axccd  45211  axccd2  45212  fzisoeu  45286  islpcn  45624  lptre2pt  45625  stoweidlem14  45999  stoweidlem35  46020  stoweidlem39  46024  stoweidlem50  46035  stoweidlem56  46041  stoweidlem59  46044  stoweidlem60  46045  fourier2  46212  qndenserrnbllem  46279  qndenserrn  46284  ovncvrrp  46549  ovnsubaddlem2  46556  hoidmvval0b  46575  hoiqssbllem3  46609  ormklocald  46859  natlocalincr  46861  tworepnotupword  46871  funressnfv  47031  imasetpreimafvbijlemfv1  47391  fundcmpsurinjpreimafv  47396  elsprel  47463  isubgredg  47854  isubgr3stgr  47963  grlimedgclnbgr  47983  grlimprclnbgredg  47985  grlimpredg  47986  grlimprclnbgrvtx  47987  grilcbri2  47999  clnbgr3stgrgrlic  48008  subthinc  49432