Theorem eximdv 1918

Description: Deduction form of Theorem 19.22 of [Margaris] p. 90, see exim 1835. See eximdh 1865 and eximd 2214 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 1781

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

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

This theorem is referenced by:  2eximdv  1920  exlimdv  1934  19.41v  1950  equvinva  2037  dfmoeu  2594  moim  2602  mo4  2625  reximdv2  3230  cgsexg  3484  spcimdv  3540  spcegv  3545  euind  3663  sselOLD  3909  reupick  4239  reximdva0  4265  uniss  4808  eusvnfb  5259  reusv2lem3  5266  axprlem1  5289  axprlem2  5290  axprlem3  5291  axpr  5294  relopabi  5658  coss1  5690  coss2  5691  ssrelrn  5727  dmss  5735  dmcosseq  5809  funssres  6368  brprcneu  6637  fv3  6663  dffv2  6733  fvn0ssdmfun  6819  dffo4  6846  dffo5  6847  funopsn  6887  fvclss  6979  fsnex  7017  f1prex  7018  f1eqcocnv  7035  f1eqcocnvOLD  7036  mapsnd  8433  enp1i  8737  en2  8738  en4  8740  marypha2  8887  brwdom3  9030  isinffi  9405  infpwfien  9473  infmap2  9629  cfub  9660  cflm  9661  cff1  9669  cfss  9676  isf32lem9  9772  axcc4  9850  acncc  9851  domtriomlem  9853  ac6s  9895  iundom2g  9951  winalim2  10107  grudomon  10228  nsmallnq  10388  prnmadd  10408  ltexprlem1  10447  ltexprlem3  10449  ltexprlem4  10450  reclem2pr  10459  dedekind  10792  xrsupsslem  12688  xrinfmsslem  12689  ishashinf  13817  coss12d  14323  supcvg  15203  vdwlem2  16308  ram0  16348  mreexexlem2d  16908  initoeu1  17263  termoeu1  17270  acsmapd  17780  acsmap2d  17781  dirge  17839  odcau  18721  ablfac2  19204  lspprat  19918  cmpsub  22005  cmpcld  22007  2ndcsep  22064  1stcelcls  22066  txcn  22231  fgcl  22483  ufildom1  22531  metustexhalf  23163  bcthlem5  23932  mbfi1flim  24327  itg2seq  24346  dchrisumlem3  26075  upgrex  26885  uhgrvd00  27324  wlkiswwlksupgr2  27663  wlklnwwlkln2lem  27668  umgrwwlks2on  27743  wpthswwlks2on  27747  frcond3  28054  frgrncvvdeqlem9  28092  ubthlem1  28653  axhcompl-zf  28781  isch3  29024  cnlnssadj  29863  acunirnmpt  30422  f1ocnt  30551  qsxpid  30978  zarclsint  31225  insiga  31506  bnj605  32289  bnj607  32298  bnj1018g  32345  bnj1018  32346  cusgredgex  32481  loop1cycl  32497  erdsze2lem1  32563  fundmpss  33122  bj-zfauscl  34367  bj-restn0  34505  dissneqlem  34757  relowlpssretop  34781  pibt2  34834  poimirlem30  35087  fdc1  35184  prdstotbnd  35232  cossss  35830  prter2  36177  lsat0cv  36329  pmapglb2N  37067  elpaddn0  37096  cdlemftr3  37861  dibglbN  38462  dihglbcpreN  38596  dihjatcclem4  38717  mapdordlem2  38933  sn-axprlem3  39401  sn-dtru  39403  dfac11  40006  neik0pk1imk0  40750  rr-spce  40910  cpcolld  40966  ax6e2ndeq  41265  fnchoice  41658  rfcnnnub  41665  eliin2f  41740  founiiun0  41817  disjinfi  41820  axccd  41861  axccd2  41862  fvelima2  41898  fzisoeu  41932  islpcn  42281  lptre2pt  42282  stoweidlem14  42656  stoweidlem35  42677  stoweidlem39  42681  stoweidlem50  42692  stoweidlem56  42698  stoweidlem59  42701  stoweidlem60  42702  fourier2  42869  qndenserrnbllem  42936  qndenserrn  42941  ovncvrrp  43203  ovnsubaddlem2  43210  hoidmvval0b  43229  hoiqssbllem3  43263  funressnfv  43635  imasetpreimafvbijlemfv1  43920  fundcmpsurinjpreimafv  43925  elsprel  43992