Theorem eximdv 1951

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

This proof depends on syntax axioms:   → wi 4  ∃wex 1811

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944

This proof depends on definitions:  df-bi 210  df-ex 1812

This theorem is used by:  2eximdv  1953  exlimdv  1967  19.41v  1983  equvinva  2064  dfmoeu  2563  moim  2572  mo4  2594  reximdv2  3175  cgsexg  3497  spcimdv  3550  spcegv  3554  euind  3684  sbcimdv  3809  reupick  4276  reximdva0  4305  uniss  4877  dfiun2g  4990  replem  5243  sepexlem  5256  eusvnfb  5358  reusv2lem3  5365  axprlem2  5389  axprlem4  5391  axpr  5392  axprlem1OLD  5393  axprglem  5397  exexneq  5406  relopabi  5804  coss1  5837  coss2  5838  ssrelrn  5880  dmss  5888  dmcosseq  5964  dmcosseqOLD  5965  funssres  6592  brprcneu  6883  brprcneuALT  6884  fv3  6911  fvelima2  6945  dffv2  6988  fvn0ssdmfun  7082  dffo4  7111  dffo5  7112  funopsn  7159  funopsnOLD  7160  fvclss  7252  fsnex  7298  f1prex  7299  f1eqcocnv  7316  mapsnd  8925  en2  9282  en4  9284  marypha2  9441  brwdom3  9586  elirrvOLD  9602  isinffi  10083  infpwfien  10151  infmap2  10305  cfub  10336  cflm  10337  cff1  10346  cfss  10353  isf32lem9  10449  axcc4  10527  acncc  10528  domtriomlem  10530  ac6s  10572  iundom2g  10634  winalim2  10791  grudomon  10912  nsmallnq  11072  prnmadd  11092  ltexprlem1  11131  ltexprlem3  11133  ltexprlem4  11134  reclem2pr  11143  dedekind  11483  xrsupsslem  13447  xrinfmsslem  13448  ishashinf  14618  hash3tpde  14648  coss12d  15137  supcvg  16037  vdwlem2  17172  ram0  17212  mreexexlem2d  17831  initoeu1  18198  termoeu1  18205  acsmapd  18740  acsmap2d  18741  dirge  18789  qsxpid  19399  odcau  19830  ablfac2  20317  lspprat  21443  lidlunin0  21527  cmpsub  23730  cmpcld  23732  2ndcsep  23790  1stcelcls  23792  txcn  23957  fgcl  24209  ufildom1  24257  metustexhalf  24887  bcthlem5  25661  mbfi1flim  26056  itg2seq  26075  dchrisumlem3  27830  upgrex  29682  uhgrvd00  30127  wlkiswwlksupgr2  30478  wlklnwwlkln2lem  30483  usgrwwlks2on  30559  umgrwwlks2on  30560  wpthswwlks2on  30565  loop1cycl  30756  frcond3  30882  frgrncvvdeqlem9  30920  ubthlem1  31484  axhcompl-zf  31612  isch3  31855  cnlnssadj  32694  ac6mapd  33271  acunirnmpt  33307  padct  33364  f1ocnt  33445  wrdpmtrlast  33707  zarclsint  34557  insiga  34823  bnj605  35590  bnj607  35599  bnj1018g  35646  bnj1018  35647  axprALT2  35795  dfac15  35824  acwer1prclem  35830  acwer1prc  35831  axsepg2  35879  axsepg4  35882  axpowg2  35886  karddom  35900  kardsdom  35901  cusgredgex  36017  erdsze2lem1  36089  ptpconn  36119  mirimanoffr  36581  fundmpss  36659  axtco1from2  37390  regsfromregtco  37453  bj-sepg  37963  bj-axseprep  38129  bj-restn0  38150  dissneqlem  38403  relowlpssretop  38427  pibt2  38480  wl-isseteq  38568  wl-dfcleq  38577  poimirlem30  38708  fdc1  38820  prdstotbnd  38868  cossss  39587  prter2  40078  lsat0cv  40230  pmapglb2N  40968  elpaddn0  40997  cdlemftr3  41762  dibglbN  42363  dihglbcpreN  42497  dihjatcclem4  42618  sticksstones3  43338  sticksstones20  43356  sn-axprlem3  43412  eu6w  43827  dfac11  44204  neik0pk1imk0  45187  rr-spce  45342  cpcolld  45382  ismnushort  45425  ax6e2ndeq  45681  ssclaxsep  46111  fnchoice  46185  rfcnnnub  46192  eliin2f  46258  founiiun0  46344  disjinfi  46346  axccd  46380  axccd2  46381  fzisoeu  46455  islpcn  46788  lptre2pt  46789  stoweidlem14  47163  stoweidlem35  47184  stoweidlem39  47188  stoweidlem50  47199  stoweidlem56  47205  stoweidlem59  47208  stoweidlem60  47209  fourier2  47376  qndenserrnbllem  47443  qndenserrn  47448  ovncvrrp  47713  ovnsubaddlem2  47720  hoidmvval0b  47739  hoiqssbllem3  47773  ormklocald  48025  tmachlem-exagreecover  48095  funressnfv  48252  imasetpreimafvbijlemfv1  48624  fundcmpsurinjpreimafv  48629  elsprel  48696  isubgredg  49103  isubgr3stgr  49212  grlimedgclnbgr  49232  grlimprclnbgredg  49234  grlimpredg  49235  grlimprclnbgrvtx  49236  grilcbri2  49248  clnbgr3stgrgrlic  49257  subthinc  50717