Theorem eximdv 1918

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

Syntax hints:   → wi 4  ∃wex 1780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

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

This theorem is referenced by:  2eximdv  1920  exlimdv  1934  19.41v  1950  equvinva  2031  dfmoeu  2531  moim  2539  mo4  2561  reximdv2  3142  cgsexg  3481  spcimdv  3543  spcegv  3547  euind  3678  sbcimdv  3805  reupick  4276  reximdva0  4302  uniss  4864  dfiun2g  4978  sepexlem  5235  eusvnfb  5329  reusv2lem3  5336  axprlem1  5359  axprlem2  5360  axprlem4  5362  axpr  5363  axprlem3OLD  5364  axprOLD  5367  exexneq  5375  relopabi  5761  coss1  5794  coss2  5795  ssrelrn  5833  dmss  5841  dmcosseq  5916  dmcosseqOLD  5917  dmcosseqOLDOLD  5918  funssres  6525  brprcneu  6812  brprcneuALT  6813  fv3  6840  fvelima2  6874  dffv2  6917  fvn0ssdmfun  7007  dffo4  7036  dffo5  7037  funopsn  7081  fvclss  7175  fsnex  7217  f1prex  7218  f1eqcocnv  7235  mapsnd  8810  en2  9164  en4  9166  marypha2  9323  brwdom3  9468  elirrv  9483  isinffi  9885  infpwfien  9953  infmap2  10108  cfub  10140  cflm  10141  cff1  10149  cfss  10156  isf32lem9  10252  axcc4  10330  acncc  10331  domtriomlem  10333  ac6s  10375  iundom2g  10431  winalim2  10587  grudomon  10708  nsmallnq  10868  prnmadd  10888  ltexprlem1  10927  ltexprlem3  10929  ltexprlem4  10930  reclem2pr  10939  dedekind  11276  xrsupsslem  13206  xrinfmsslem  13207  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  19516  ablfac2  20003  lspprat  21090  cmpsub  23315  cmpcld  23317  2ndcsep  23374  1stcelcls  23376  txcn  23541  fgcl  23793  ufildom1  23841  metustexhalf  24471  bcthlem5  25255  mbfi1flim  25651  itg2seq  25670  dchrisumlem3  27429  upgrex  29070  uhgrvd00  29513  wlkiswwlksupgr2  29855  wlklnwwlkln2lem  29860  usgrwwlks2on  29936  umgrwwlks2on  29937  wpthswwlks2on  29942  frcond3  30249  frgrncvvdeqlem9  30287  ubthlem1  30850  axhcompl-zf  30978  isch3  31221  cnlnssadj  32060  ac6mapd  32606  acunirnmpt  32641  f1ocnt  32782  wrdpmtrlast  33062  qsxpid  33327  zarclsint  33885  insiga  34150  bnj605  34919  bnj607  34928  bnj1018g  34975  bnj1018  34976  cusgredgex  35166  loop1cycl  35181  erdsze2lem1  35247  fundmpss  35811  bj-zfauscl  36968  bj-restn0  37134  dissneqlem  37384  relowlpssretop  37408  pibt2  37461  wl-isseteq  37549  poimirlem30  37700  fdc1  37796  prdstotbnd  37844  cossss  38537  prter2  38990  lsat0cv  39142  pmapglb2N  39880  elpaddn0  39909  cdlemftr3  40674  dibglbN  41275  dihglbcpreN  41409  dihjatcclem4  41530  mapdordlem2  41746  sticksstones3  42251  sticksstones20  42269  sn-axprlem3  42320  eu6w  42779  dfac11  43165  neik0pk1imk0  44150  rr-spce  44307  cpcolld  44361  ismnushort  44404  ax6e2ndeq  44662  ssclaxsep  45085  fnchoice  45136  rfcnnnub  45143  eliin2f  45211  founiiun0  45297  disjinfi  45299  axccd  45336  axccd2  45337  fzisoeu  45411  islpcn  45747  lptre2pt  45748  stoweidlem14  46122  stoweidlem35  46143  stoweidlem39  46147  stoweidlem50  46158  stoweidlem56  46164  stoweidlem59  46167  stoweidlem60  46168  fourier2  46335  qndenserrnbllem  46402  qndenserrn  46407  ovncvrrp  46672  ovnsubaddlem2  46679  hoidmvval0b  46698  hoiqssbllem3  46732  ormklocald  46982  natlocalincr  46984  funressnfv  47153  imasetpreimafvbijlemfv1  47513  fundcmpsurinjpreimafv  47518  elsprel  47585  isubgredg  47976  isubgr3stgr  48085  grlimedgclnbgr  48105  grlimprclnbgredg  48107  grlimpredg  48108  grlimprclnbgrvtx  48109  grilcbri2  48121  clnbgr3stgrgrlic  48130  subthinc  49554