Theorem eximdv 1944

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

Syntax hints:   → wi 4  ∃wex 1806

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937

This theorem depends on definitions:  df-bi 210  df-ex 1807

This theorem is referenced by:  2eximdv  1946  exlimdv  1960  19.41v  1976  equvinva  2057  dfmoeu  2569  moim  2578  mo4  2600  reximdv2  3181  cgsexg  3507  spcimdv  3561  spcegv  3565  euind  3696  sbcimdv  3821  reupick  4290  reximdva0  4318  uniss  4884  dfiun2g  4998  replem  5253  sepexlem  5264  eusvnfb  5365  reusv2lem3  5372  axprlem2  5396  axprlem4  5398  axpr  5399  axprlem1OLD  5400  axprlem3OLD  5401  axprOLD  5404  axprglem  5408  exexneq  5417  relopabi  5810  coss1  5842  coss2  5843  ssrelrn  5885  dmss  5893  dmcosseq  5969  dmcosseqOLD  5970  funssres  6581  brprcneu  6872  brprcneuALT  6873  fv3  6900  fvelima2  6934  dffv2  6977  fvn0ssdmfun  7070  dffo4  7099  dffo5  7100  funopsn  7145  funopsnOLD  7146  fvclss  7240  fsnex  7282  f1prex  7283  f1eqcocnv  7300  mapsnd  8884  en2  9240  en4  9242  marypha2  9399  brwdom3  9544  elirrvOLD  9560  isinffi  9978  infpwfien  10046  infmap2  10200  cfub  10232  cflm  10233  cff1  10242  cfss  10249  isf32lem9  10345  axcc4  10423  acncc  10424  domtriomlem  10426  ac6s  10468  iundom2g  10524  winalim2  10681  grudomon  10802  nsmallnq  10962  prnmadd  10982  ltexprlem1  11021  ltexprlem3  11023  ltexprlem4  11024  reclem2pr  11033  dedekind  11373  xrsupsslem  13333  xrinfmsslem  13334  ishashinf  14500  hash3tpde  14530  coss12d  15009  supcvg  15910  vdwlem2  17042  ram0  17082  mreexexlem2d  17701  initoeu1  18068  termoeu1  18075  acsmapd  18610  acsmap2d  18611  dirge  18659  qsxpid  19243  odcau  19674  ablfac2  20161  lspprat  21255  lidlunin0  21339  cmpsub  23526  cmpcld  23528  2ndcsep  23585  1stcelcls  23587  txcn  23752  fgcl  24004  ufildom1  24052  metustexhalf  24682  bcthlem5  25456  mbfi1flim  25851  itg2seq  25870  dchrisumlem3  27621  upgrex  29383  uhgrvd00  29825  wlkiswwlksupgr2  30167  wlklnwwlkln2lem  30172  usgrwwlks2on  30248  umgrwwlks2on  30249  wpthswwlks2on  30254  frcond3  30561  frgrncvvdeqlem9  30599  ubthlem1  31163  axhcompl-zf  31291  isch3  31534  cnlnssadj  32373  ac6mapd  32909  acunirnmpt  32945  padct  33004  f1ocnt  33086  wrdpmtrlast  33354  zarclsint  34207  insiga  34472  bnj605  35240  bnj607  35249  bnj1018g  35296  bnj1018  35297  axprALT2  35445  axsepg2  35476  axsepg4  35479  axpowg2  35483  cusgredgex  35513  loop1cycl  35528  erdsze2lem1  35594  fundmpss  36158  axtco1from2  36875  regsfromregtco  36938  bj-zfauscl  37448  bj-axseprep  37599  bj-restn0  37620  dissneqlem  37874  relowlpssretop  37898  pibt2  37951  wl-isseteq  38039  wl-dfcleq  38048  poimirlem30  38189  fdc1  38285  prdstotbnd  38333  cossss  39054  prter2  39545  lsat0cv  39697  pmapglb2N  40435  elpaddn0  40464  cdlemftr3  41229  dibglbN  41830  dihglbcpreN  41964  dihjatcclem4  42085  sticksstones3  42805  sticksstones20  42823  sn-axprlem3  42879  eu6w  43300  dfac11  43681  neik0pk1imk0  44665  rr-spce  44820  cpcolld  44860  ismnushort  44903  ax6e2ndeq  45160  ssclaxsep  45583  fnchoice  45641  rfcnnnub  45648  eliin2f  45714  founiiun0  45800  disjinfi  45802  axccd  45836  axccd2  45837  fzisoeu  45911  islpcn  46245  lptre2pt  46246  stoweidlem14  46620  stoweidlem35  46641  stoweidlem39  46645  stoweidlem50  46656  stoweidlem56  46662  stoweidlem59  46665  stoweidlem60  46666  fourier2  46833  qndenserrnbllem  46900  qndenserrn  46905  ovncvrrp  47170  ovnsubaddlem2  47177  hoidmvval0b  47196  hoiqssbllem3  47230  ormklocald  47482  natlocalincr  47484  funressnfv  47669  imasetpreimafvbijlemfv1  48041  fundcmpsurinjpreimafv  48046  elsprel  48113  isubgredg  48520  isubgr3stgr  48629  grlimedgclnbgr  48649  grlimprclnbgredg  48651  grlimpredg  48652  grlimprclnbgrvtx  48653  grilcbri2  48665  clnbgr3stgrgrlic  48674  subthinc  50106