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  4278  reximdva0  4304  uniss  4866  dfiun2g  4980  sepexlem  5239  eusvnfb  5333  reusv2lem3  5340  axprlem1  5363  axprlem2  5364  axprlem4  5366  axpr  5367  axprlem3OLD  5368  axprOLD  5371  exexneq  5379  relopabi  5767  coss1  5800  coss2  5801  ssrelrn  5839  dmss  5847  dmcosseq  5922  dmcosseqOLD  5923  dmcosseqOLDOLD  5924  funssres  6531  brprcneu  6818  brprcneuALT  6819  fv3  6846  fvelima2  6880  dffv2  6923  fvn0ssdmfun  7013  dffo4  7042  dffo5  7043  funopsn  7087  fvclss  7181  fsnex  7223  f1prex  7224  f1eqcocnv  7241  mapsnd  8816  en2  9170  en4  9172  marypha2  9329  brwdom3  9474  elirrv  9489  isinffi  9891  infpwfien  9959  infmap2  10114  cfub  10146  cflm  10147  cff1  10155  cfss  10162  isf32lem9  10258  axcc4  10336  acncc  10337  domtriomlem  10339  ac6s  10381  iundom2g  10437  winalim2  10593  grudomon  10714  nsmallnq  10874  prnmadd  10894  ltexprlem1  10933  ltexprlem3  10935  ltexprlem4  10936  reclem2pr  10945  dedekind  11282  xrsupsslem  13212  xrinfmsslem  13213  ishashinf  14376  hash3tpde  14406  coss12d  14885  supcvg  15769  vdwlem2  16900  ram0  16940  mreexexlem2d  17557  initoeu1  17924  termoeu1  17931  acsmapd  18466  acsmap2d  18467  dirge  18515  odcau  19522  ablfac2  20009  lspprat  21096  cmpsub  23321  cmpcld  23323  2ndcsep  23380  1stcelcls  23382  txcn  23547  fgcl  23799  ufildom1  23847  metustexhalf  24477  bcthlem5  25261  mbfi1flim  25657  itg2seq  25676  dchrisumlem3  27435  upgrex  29077  uhgrvd00  29520  wlkiswwlksupgr2  29862  wlklnwwlkln2lem  29867  usgrwwlks2on  29943  umgrwwlks2on  29944  wpthswwlks2on  29949  frcond3  30256  frgrncvvdeqlem9  30294  ubthlem1  30857  axhcompl-zf  30985  isch3  31228  cnlnssadj  32067  ac6mapd  32613  acunirnmpt  32648  f1ocnt  32789  wrdpmtrlast  33069  qsxpid  33334  zarclsint  33892  insiga  34157  bnj605  34926  bnj607  34935  bnj1018g  34982  bnj1018  34983  cusgredgex  35173  loop1cycl  35188  erdsze2lem1  35254  fundmpss  35818  bj-zfauscl  36975  bj-restn0  37141  dissneqlem  37391  relowlpssretop  37415  pibt2  37468  wl-isseteq  37556  poimirlem30  37696  fdc1  37792  prdstotbnd  37840  cossss  38533  prter2  38986  lsat0cv  39138  pmapglb2N  39876  elpaddn0  39905  cdlemftr3  40670  dibglbN  41271  dihglbcpreN  41405  dihjatcclem4  41526  sticksstones3  42247  sticksstones20  42265  sn-axprlem3  42316  eu6w  42775  dfac11  43160  neik0pk1imk0  44145  rr-spce  44302  cpcolld  44356  ismnushort  44399  ax6e2ndeq  44657  ssclaxsep  45080  fnchoice  45131  rfcnnnub  45138  eliin2f  45206  founiiun0  45292  disjinfi  45294  axccd  45331  axccd2  45332  fzisoeu  45406  islpcn  45742  lptre2pt  45743  stoweidlem14  46117  stoweidlem35  46138  stoweidlem39  46142  stoweidlem50  46153  stoweidlem56  46159  stoweidlem59  46162  stoweidlem60  46163  fourier2  46330  qndenserrnbllem  46397  qndenserrn  46402  ovncvrrp  46667  ovnsubaddlem2  46674  hoidmvval0b  46693  hoiqssbllem3  46727  ormklocald  46977  natlocalincr  46979  funressnfv  47148  imasetpreimafvbijlemfv1  47508  fundcmpsurinjpreimafv  47513  elsprel  47580  isubgredg  47971  isubgr3stgr  48080  grlimedgclnbgr  48100  grlimprclnbgredg  48102  grlimpredg  48103  grlimprclnbgrvtx  48104  grilcbri2  48116  clnbgr3stgrgrlic  48125  subthinc  49549