Theorem eximdv 1937

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

Syntax hints:   → wi 4  ∃wex 1799

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930

This theorem depends on definitions:  df-bi 209  df-ex 1800

This theorem is referenced by:  2eximdv  1939  exlimdv  1953  19.41v  1969  equvinva  2050  dfmoeu  2562  moim  2571  mo4  2593  reximdv2  3172  cgsexg  3498  spcimdv  3552  spcegv  3556  euind  3687  sbcimdv  3812  reupick  4281  reximdva0  4308  uniss  4873  dfiun2g  4987  replem  5238  sepexlem  5249  eusvnfb  5350  reusv2lem3  5357  axprlem2  5381  axprlem4  5383  axpr  5384  axprlem1OLD  5385  axprlem3OLD  5386  axprOLD  5389  axprglem  5393  exexneq  5402  relopabi  5795  coss1  5827  coss2  5828  ssrelrn  5870  dmss  5878  dmcosseq  5954  dmcosseqOLD  5955  dmcosseqOLDOLD  5956  funssres  6565  brprcneu  6857  brprcneuALT  6858  fv3  6885  fvelima2  6919  dffv2  6962  fvn0ssdmfun  7055  dffo4  7084  dffo5  7085  funopsn  7130  funopsnOLD  7131  fvclss  7225  fsnex  7267  f1prex  7268  f1eqcocnv  7285  mapsnd  8868  en2  9224  en4  9226  marypha2  9385  brwdom3  9530  elirrvOLD  9546  isinffi  9950  infpwfien  10018  infmap2  10173  cfub  10205  cflm  10206  cff1  10215  cfss  10222  isf32lem9  10318  axcc4  10396  acncc  10397  domtriomlem  10399  ac6s  10441  iundom2g  10497  winalim2  10654  grudomon  10775  nsmallnq  10935  prnmadd  10955  ltexprlem1  10994  ltexprlem3  10996  ltexprlem4  10997  reclem2pr  11006  dedekind  11346  xrsupsslem  13310  xrinfmsslem  13311  ishashinf  14476  hash3tpde  14506  coss12d  14985  supcvg  15886  vdwlem2  17018  ram0  17058  mreexexlem2d  17677  initoeu1  18044  termoeu1  18051  acsmapd  18586  acsmap2d  18587  dirge  18635  odcau  19644  ablfac2  20131  lspprat  21223  cmpsub  23460  cmpcld  23462  2ndcsep  23519  1stcelcls  23521  txcn  23686  fgcl  23938  ufildom1  23986  metustexhalf  24616  bcthlem5  25390  mbfi1flim  25785  itg2seq  25804  dchrisumlem3  27555  upgrex  29293  uhgrvd00  29735  wlkiswwlksupgr2  30077  wlklnwwlkln2lem  30082  usgrwwlks2on  30158  umgrwwlks2on  30159  wpthswwlks2on  30164  frcond3  30471  frgrncvvdeqlem9  30509  ubthlem1  31073  axhcompl-zf  31201  isch3  31444  cnlnssadj  32283  ac6mapd  32825  acunirnmpt  32861  padct  32920  f1ocnt  33002  wrdpmtrlast  33273  qsxpid  33548  zarclsint  34169  insiga  34434  bnj605  35202  bnj607  35211  bnj1018g  35258  bnj1018  35259  axprALT2  35405  axsepg2  35436  axsepg4  35439  axpowg2  35443  cusgredgex  35472  loop1cycl  35487  erdsze2lem1  35553  fundmpss  36117  axtco1from2  36835  regsfromregtco  36898  bj-zfauscl  37409  bj-axseprep  37559  bj-restn0  37580  dissneqlem  37834  relowlpssretop  37858  pibt2  37911  wl-isseteq  37999  wl-dfcleq  38008  poimirlem30  38149  fdc1  38245  prdstotbnd  38293  cossss  39014  prter2  39505  lsat0cv  39657  pmapglb2N  40395  elpaddn0  40424  cdlemftr3  41189  dibglbN  41790  dihglbcpreN  41924  dihjatcclem4  42045  sticksstones3  42765  sticksstones20  42783  sn-axprlem3  42837  eu6w  43258  dfac11  43639  neik0pk1imk0  44623  rr-spce  44780  cpcolld  44834  ismnushort  44877  ax6e2ndeq  45135  ssclaxsep  45558  fnchoice  45609  rfcnnnub  45616  eliin2f  45682  founiiun0  45768  disjinfi  45770  axccd  45804  axccd2  45805  fzisoeu  45879  islpcn  46213  lptre2pt  46214  stoweidlem14  46588  stoweidlem35  46609  stoweidlem39  46613  stoweidlem50  46624  stoweidlem56  46630  stoweidlem59  46633  stoweidlem60  46634  fourier2  46801  qndenserrnbllem  46868  qndenserrn  46873  ovncvrrp  47138  ovnsubaddlem2  47145  hoidmvval0b  47164  hoiqssbllem3  47198  ormklocald  47450  natlocalincr  47452  funressnfv  47637  imasetpreimafvbijlemfv1  48009  fundcmpsurinjpreimafv  48014  elsprel  48081  isubgredg  48488  isubgr3stgr  48597  grlimedgclnbgr  48617  grlimprclnbgredg  48619  grlimpredg  48620  grlimprclnbgrvtx  48621  grilcbri2  48633  clnbgr3stgrgrlic  48642  subthinc  50064