Theorem eximdv 1947

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

Syntax hints:   → wi 4  ∃wex 1809

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940

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

This theorem is referenced by:  2eximdv  1949  exlimdv  1963  19.41v  1979  equvinva  2060  dfmoeu  2563  moim  2572  mo4  2594  reximdv2  3175  cgsexg  3499  spcimdv  3552  spcegv  3556  euind  3687  sbcimdv  3812  reupick  4282  reximdva0  4310  uniss  4880  dfiun2g  4994  replem  5249  sepexlem  5262  eusvnfb  5364  reusv2lem3  5371  axprlem2  5395  axprlem4  5397  axpr  5398  axprlem1OLD  5399  axprlem3OLD  5400  axprOLD  5403  axprglem  5407  exexneq  5416  relopabi  5809  coss1  5841  coss2  5842  ssrelrn  5884  dmss  5892  dmcosseq  5968  dmcosseqOLD  5969  funssres  6580  brprcneu  6871  brprcneuALT  6872  fv3  6899  fvelima2  6933  dffv2  6976  fvn0ssdmfun  7069  dffo4  7098  dffo5  7099  funopsn  7144  funopsnOLD  7145  fvclss  7239  fsnex  7281  f1prex  7282  f1eqcocnv  7299  mapsnd  8880  en2  9236  en4  9238  marypha2  9395  brwdom3  9540  elirrvOLD  9556  isinffi  9974  infpwfien  10042  infmap2  10196  cfub  10227  cflm  10228  cff1  10237  cfss  10244  isf32lem9  10340  axcc4  10418  acncc  10419  domtriomlem  10421  ac6s  10463  iundom2g  10519  winalim2  10676  grudomon  10797  nsmallnq  10957  prnmadd  10977  ltexprlem1  11016  ltexprlem3  11018  ltexprlem4  11019  reclem2pr  11028  dedekind  11368  xrsupsslem  13328  xrinfmsslem  13329  ishashinf  14496  hash3tpde  14526  coss12d  15005  supcvg  15906  vdwlem2  17037  ram0  17077  mreexexlem2d  17696  initoeu1  18063  termoeu1  18070  acsmapd  18605  acsmap2d  18606  dirge  18654  qsxpid  19238  odcau  19669  ablfac2  20156  lspprat  21277  lidlunin0  21361  cmpsub  23557  cmpcld  23559  2ndcsep  23616  1stcelcls  23618  txcn  23783  fgcl  24035  ufildom1  24083  metustexhalf  24713  bcthlem5  25487  mbfi1flim  25882  itg2seq  25901  dchrisumlem3  27655  upgrex  29442  uhgrvd00  29884  wlkiswwlksupgr2  30226  wlklnwwlkln2lem  30231  usgrwwlks2on  30307  umgrwwlks2on  30308  wpthswwlks2on  30313  frcond3  30620  frgrncvvdeqlem9  30658  ubthlem1  31222  axhcompl-zf  31350  isch3  31593  cnlnssadj  32432  ac6mapd  32968  acunirnmpt  33004  padct  33063  f1ocnt  33145  wrdpmtrlast  33413  zarclsint  34262  insiga  34527  bnj605  35295  bnj607  35304  bnj1018g  35351  bnj1018  35352  axprALT2  35503  axsepg2  35553  axsepg4  35556  axpowg2  35560  karddom  35574  kardsdom  35575  cusgredgex  35614  loop1cycl  35629  erdsze2lem1  35695  fundmpss  36259  axtco1from2  37006  regsfromregtco  37069  bj-sepg  37579  bj-axseprep  37731  bj-restn0  37752  dissneqlem  38006  relowlpssretop  38030  pibt2  38083  wl-isseteq  38171  wl-dfcleq  38180  poimirlem30  38321  fdc1  38417  prdstotbnd  38465  cossss  39184  prter2  39675  lsat0cv  39827  pmapglb2N  40565  elpaddn0  40594  cdlemftr3  41359  dibglbN  41960  dihglbcpreN  42094  dihjatcclem4  42215  sticksstones3  42935  sticksstones20  42953  sn-axprlem3  43009  eu6w  43428  dfac11  43809  neik0pk1imk0  44793  rr-spce  44948  cpcolld  44988  ismnushort  45031  ax6e2ndeq  45288  ssclaxsep  45711  fnchoice  45769  rfcnnnub  45776  eliin2f  45842  founiiun0  45928  disjinfi  45930  axccd  45964  axccd2  45965  fzisoeu  46039  islpcn  46373  lptre2pt  46374  stoweidlem14  46748  stoweidlem35  46769  stoweidlem39  46773  stoweidlem50  46784  stoweidlem56  46790  stoweidlem59  46793  stoweidlem60  46794  fourier2  46961  qndenserrnbllem  47028  qndenserrn  47033  ovncvrrp  47298  ovnsubaddlem2  47305  hoidmvval0b  47324  hoiqssbllem3  47358  ormklocald  47610  natlocalincr  47612  funressnfv  47800  imasetpreimafvbijlemfv1  48172  fundcmpsurinjpreimafv  48177  elsprel  48244  isubgredg  48651  isubgr3stgr  48760  grlimedgclnbgr  48780  grlimprclnbgredg  48782  grlimpredg  48783  grlimprclnbgrvtx  48784  grilcbri2  48796  clnbgr3stgrgrlic  48805  subthinc  50241