Theorem eximdv 1917

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

Syntax hints:   → wi 4  ∃wex 1779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

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

This theorem is referenced by:  2eximdv  1919  exlimdv  1933  19.41v  1949  equvinva  2030  dfmoeu  2529  moim  2537  mo4  2559  reximdv2  3143  cgsexg  3489  spcimdv  3556  spcegv  3560  euind  3692  sbcimdv  3819  reupick  4288  reximdva0  4314  uniss  4875  dfiun2g  4990  sepexlem  5249  eusvnfb  5343  reusv2lem3  5350  axprlem1  5373  axprlem2  5374  axprlem4  5376  axpr  5377  axprlem3OLD  5378  axprOLD  5381  exexneq  5389  relopabi  5776  coss1  5809  coss2  5810  ssrelrn  5848  dmss  5856  dmcosseq  5929  dmcosseqOLD  5930  funssres  6544  brprcneu  6830  brprcneuALT  6831  fv3  6858  fvelima2  6895  dffv2  6938  fvn0ssdmfun  7028  dffo4  7057  dffo5  7058  funopsn  7102  fvclss  7197  fsnex  7240  f1prex  7241  f1eqcocnv  7258  mapsnd  8836  enp1iOLD  9201  en2  9202  en4  9204  marypha2  9366  brwdom3  9511  isinffi  9921  infpwfien  9991  infmap2  10146  cfub  10178  cflm  10179  cff1  10187  cfss  10194  isf32lem9  10290  axcc4  10368  acncc  10369  domtriomlem  10371  ac6s  10413  iundom2g  10469  winalim2  10625  grudomon  10746  nsmallnq  10906  prnmadd  10926  ltexprlem1  10965  ltexprlem3  10967  ltexprlem4  10968  reclem2pr  10977  dedekind  11313  xrsupsslem  13243  xrinfmsslem  13244  ishashinf  14404  hash3tpde  14434  coss12d  14914  supcvg  15798  vdwlem2  16929  ram0  16969  mreexexlem2d  17586  initoeu1  17953  termoeu1  17960  acsmapd  18495  acsmap2d  18496  dirge  18544  odcau  19518  ablfac2  20005  lspprat  21095  cmpsub  23320  cmpcld  23322  2ndcsep  23379  1stcelcls  23381  txcn  23546  fgcl  23798  ufildom1  23846  metustexhalf  24477  bcthlem5  25261  mbfi1flim  25657  itg2seq  25676  dchrisumlem3  27435  upgrex  29072  uhgrvd00  29515  wlkiswwlksupgr2  29857  wlklnwwlkln2lem  29862  umgrwwlks2on  29937  wpthswwlks2on  29941  frcond3  30248  frgrncvvdeqlem9  30286  ubthlem1  30849  axhcompl-zf  30977  isch3  31220  cnlnssadj  32059  ac6mapd  32599  acunirnmpt  32633  f1ocnt  32775  wrdpmtrlast  33065  qsxpid  33326  zarclsint  33855  insiga  34120  bnj605  34890  bnj607  34899  bnj1018g  34946  bnj1018  34947  cusgredgex  35102  loop1cycl  35117  erdsze2lem1  35183  fundmpss  35747  bj-zfauscl  36905  bj-restn0  37071  dissneqlem  37321  relowlpssretop  37345  pibt2  37398  wl-isseteq  37486  poimirlem30  37637  fdc1  37733  prdstotbnd  37781  cossss  38409  prter2  38867  lsat0cv  39019  pmapglb2N  39758  elpaddn0  39787  cdlemftr3  40552  dibglbN  41153  dihglbcpreN  41287  dihjatcclem4  41408  mapdordlem2  41624  sticksstones3  42129  sticksstones20  42147  sn-axprlem3  42198  eu6w  42657  dfac11  43044  neik0pk1imk0  44029  rr-spce  44186  cpcolld  44240  ismnushort  44283  ax6e2ndeq  44542  ssclaxsep  44965  fnchoice  45016  rfcnnnub  45023  eliin2f  45091  founiiun0  45177  disjinfi  45179  axccd  45216  axccd2  45217  fzisoeu  45291  islpcn  45630  lptre2pt  45631  stoweidlem14  46005  stoweidlem35  46026  stoweidlem39  46030  stoweidlem50  46041  stoweidlem56  46047  stoweidlem59  46050  stoweidlem60  46051  fourier2  46218  qndenserrnbllem  46285  qndenserrn  46290  ovncvrrp  46555  ovnsubaddlem2  46562  hoidmvval0b  46581  hoiqssbllem3  46615  ormklocald  46865  natlocalincr  46867  tworepnotupword  46877  funressnfv  47037  imasetpreimafvbijlemfv1  47397  fundcmpsurinjpreimafv  47402  elsprel  47469  isubgredg  47859  isubgr3stgr  47967  grilcbri2  47996  clnbgr3stgrgrlic  48004  subthinc  49425