Theorem eximdv 1921

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

Syntax hints:   → wi 4  ∃wex 1782

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-ex 1783

This theorem is referenced by:  2eximdv  1923  exlimdv  1937  19.41v  1954  equvinva  2034  dfmoeu  2531  moim  2539  mo4  2561  reximdv2  3165  cgsexg  3519  spcimdv  3584  spcegv  3588  euind  3721  sbcimdv  3852  sselOLD  3977  reupick  4319  reximdva0  4352  uniss  4917  dfiun2g  5034  eusvnfb  5392  reusv2lem3  5399  axprlem1  5422  axprlem2  5423  axprlem3  5424  axpr  5427  exexneq  5435  relopabi  5823  coss1  5856  coss2  5857  ssrelrn  5895  dmss  5903  dmcosseq  5973  funssres  6593  brprcneu  6882  brprcneuALT  6883  fv3  6910  dffv2  6987  fvn0ssdmfun  7077  dffo4  7105  dffo5  7106  funopsn  7146  fvclss  7241  fsnex  7281  f1prex  7282  f1eqcocnv  7299  f1eqcocnvOLD  7300  mapsnd  8880  enp1iOLD  9280  en2  9281  en4  9283  marypha2  9434  brwdom3  9577  isinffi  9987  infpwfien  10057  infmap2  10213  cfub  10244  cflm  10245  cff1  10253  cfss  10260  isf32lem9  10356  axcc4  10434  acncc  10435  domtriomlem  10437  ac6s  10479  iundom2g  10535  winalim2  10691  grudomon  10812  nsmallnq  10972  prnmadd  10992  ltexprlem1  11031  ltexprlem3  11033  ltexprlem4  11034  reclem2pr  11043  dedekind  11377  xrsupsslem  13286  xrinfmsslem  13287  ishashinf  14424  coss12d  14919  supcvg  15802  vdwlem2  16915  ram0  16955  mreexexlem2d  17589  initoeu1  17961  termoeu1  17968  acsmapd  18507  acsmap2d  18508  dirge  18556  odcau  19472  ablfac2  19959  lspprat  20766  cmpsub  22904  cmpcld  22906  2ndcsep  22963  1stcelcls  22965  txcn  23130  fgcl  23382  ufildom1  23430  metustexhalf  24065  bcthlem5  24845  mbfi1flim  25241  itg2seq  25260  dchrisumlem3  26994  upgrex  28383  uhgrvd00  28822  wlkiswwlksupgr2  29162  wlklnwwlkln2lem  29167  umgrwwlks2on  29242  wpthswwlks2on  29246  frcond3  29553  frgrncvvdeqlem9  29591  ubthlem1  30154  axhcompl-zf  30282  isch3  30525  cnlnssadj  31364  acunirnmpt  31915  f1ocnt  32044  qsxpid  32505  zarclsint  32883  insiga  33166  bnj605  33949  bnj607  33958  bnj1018g  34005  bnj1018  34006  cusgredgex  34143  loop1cycl  34159  erdsze2lem1  34225  fundmpss  34769  bj-zfauscl  35852  bj-restn0  36019  dissneqlem  36269  relowlpssretop  36293  pibt2  36346  poimirlem30  36566  fdc1  36662  prdstotbnd  36710  cossss  37343  prter2  37799  lsat0cv  37951  pmapglb2N  38690  elpaddn0  38719  cdlemftr3  39484  dibglbN  40085  dihglbcpreN  40219  dihjatcclem4  40340  mapdordlem2  40556  sticksstones3  41012  sticksstones20  41030  sn-axprlem3  41082  dfac11  41852  neik0pk1imk0  42846  rr-spce  43004  cpcolld  43065  ismnushort  43108  ax6e2ndeq  43368  fnchoice  43761  rfcnnnub  43768  eliin2f  43841  founiiun0  43936  disjinfi  43939  axccd  43976  axccd2  43977  fvelima2  44012  fzisoeu  44058  islpcn  44403  lptre2pt  44404  stoweidlem14  44778  stoweidlem35  44799  stoweidlem39  44803  stoweidlem50  44814  stoweidlem56  44820  stoweidlem59  44823  stoweidlem60  44824  fourier2  44991  qndenserrnbllem  45058  qndenserrn  45063  ovncvrrp  45328  ovnsubaddlem2  45335  hoidmvval0b  45354  hoiqssbllem3  45388  natlocalincr  45638  tworepnotupword  45648  funressnfv  45801  imasetpreimafvbijlemfv1  46119  fundcmpsurinjpreimafv  46124  elsprel  46191  subthinc  47708