Theorem eximdv 1950

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

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

This theorem is used by:  2eximdv  1952  exlimdv  1966  19.41v  1982  equvinva  2063  dfmoeu  2560  moim  2569  mo4  2591  reximdv2  3172  cgsexg  3494  spcimdv  3547  spcegv  3551  euind  3682  sbcimdv  3807  reupick  4275  reximdva0  4303  uniss  4875  dfiun2g  4988  replem  5243  sepexlem  5256  eusvnfb  5358  reusv2lem3  5365  axprlem2  5389  axprlem4  5391  axpr  5392  axprlem1OLD  5393  axprlem3OLD  5394  axprOLD  5397  axprglem  5401  exexneq  5410  relopabi  5803  coss1  5835  coss2  5836  ssrelrn  5878  dmss  5886  dmcosseq  5962  dmcosseqOLD  5963  funssres  6578  brprcneu  6869  brprcneuALT  6870  fv3  6897  fvelima2  6931  dffv2  6974  fvn0ssdmfun  7068  dffo4  7097  dffo5  7098  funopsn  7145  funopsnOLD  7146  fvclss  7239  fsnex  7285  f1prex  7286  f1eqcocnv  7303  mapsnd  8894  en2  9251  en4  9253  marypha2  9410  brwdom3  9555  elirrvOLD  9571  isinffi  9998  infpwfien  10066  infmap2  10220  cfub  10251  cflm  10252  cff1  10261  cfss  10268  isf32lem9  10364  axcc4  10442  acncc  10443  domtriomlem  10445  ac6s  10487  iundom2g  10549  winalim2  10706  grudomon  10827  nsmallnq  10987  prnmadd  11007  ltexprlem1  11046  ltexprlem3  11048  ltexprlem4  11049  reclem2pr  11058  dedekind  11398  xrsupsslem  13360  xrinfmsslem  13361  ishashinf  14529  hash3tpde  14559  coss12d  15046  supcvg  15946  vdwlem2  17075  ram0  17115  mreexexlem2d  17734  initoeu1  18101  termoeu1  18108  acsmapd  18643  acsmap2d  18644  dirge  18692  qsxpid  19301  odcau  19732  ablfac2  20219  lspprat  21341  lidlunin0  21425  cmpsub  23626  cmpcld  23628  2ndcsep  23686  1stcelcls  23688  txcn  23853  fgcl  24105  ufildom1  24153  metustexhalf  24783  bcthlem5  25557  mbfi1flim  25952  itg2seq  25971  dchrisumlem3  27728  upgrex  29550  uhgrvd00  29995  wlkiswwlksupgr2  30346  wlklnwwlkln2lem  30351  usgrwwlks2on  30427  umgrwwlks2on  30428  wpthswwlks2on  30433  loop1cycl  30624  frcond3  30750  frgrncvvdeqlem9  30788  ubthlem1  31352  axhcompl-zf  31480  isch3  31723  cnlnssadj  32562  ac6mapd  33097  acunirnmpt  33133  padct  33190  f1ocnt  33272  wrdpmtrlast  33534  zarclsint  34383  insiga  34649  bnj605  35417  bnj607  35426  bnj1018g  35473  bnj1018  35474  axprALT2  35618  axsepg2  35667  axsepg4  35670  axpowg2  35674  karddom  35688  kardsdom  35689  cusgredgex  35721  erdsze2lem1  35783  fundmpss  36347  axtco1from2  37095  regsfromregtco  37158  bj-sepg  37668  bj-axseprep  37820  bj-restn0  37841  dissneqlem  38095  relowlpssretop  38119  pibt2  38172  wl-isseteq  38260  wl-dfcleq  38269  poimirlem30  38400  fdc1  38497  prdstotbnd  38545  cossss  39264  prter2  39755  lsat0cv  39907  pmapglb2N  40645  elpaddn0  40674  cdlemftr3  41439  dibglbN  42040  dihglbcpreN  42174  dihjatcclem4  42295  sticksstones3  43015  sticksstones20  43033  sn-axprlem3  43089  eu6w  43523  dfac11  43904  neik0pk1imk0  44888  rr-spce  45043  cpcolld  45083  ismnushort  45126  ax6e2ndeq  45383  ssclaxsep  45806  fnchoice  45864  rfcnnnub  45871  eliin2f  45937  founiiun0  46023  disjinfi  46025  axccd  46059  axccd2  46060  fzisoeu  46134  islpcn  46468  lptre2pt  46469  stoweidlem14  46843  stoweidlem35  46864  stoweidlem39  46868  stoweidlem50  46879  stoweidlem56  46885  stoweidlem59  46888  stoweidlem60  46889  fourier2  47056  qndenserrnbllem  47123  qndenserrn  47128  ovncvrrp  47393  ovnsubaddlem2  47400  hoidmvval0b  47419  hoiqssbllem3  47453  ormklocald  47705  tmachlem-exagreecover  47775  funressnfv  47932  imasetpreimafvbijlemfv1  48304  fundcmpsurinjpreimafv  48309  elsprel  48376  isubgredg  48783  isubgr3stgr  48892  grlimedgclnbgr  48912  grlimprclnbgredg  48914  grlimpredg  48915  grlimprclnbgrvtx  48916  grilcbri2  48928  clnbgr3stgrgrlic  48937  subthinc  50370