Theorem eximdv 1914

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

Syntax hints:   → wi 4  ∃wex 1776

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907

This theorem depends on definitions:  df-bi 209  df-ex 1777

This theorem is referenced by:  2eximdv  1916  exlimdv  1930  19.41v  1946  equvinva  2033  sbimdvOLD  2512  dfmoeu  2614  moim  2622  mo4  2646  reximdv2  3271  cgsexg  3537  spcimdv  3591  spcegv  3596  euind  3714  ssel  3960  reupick  4286  reximdva0  4311  uniss  4845  eusvnfb  5293  reusv2lem3  5300  axprlem1  5323  axprlem2  5324  axprlem3  5325  axpr  5328  relopabi  5693  coss1  5725  coss2  5726  ssrelrn  5762  dmss  5770  dmcosseq  5843  funssres  6397  brprcneu  6661  fv3  6687  dffv2  6755  fvn0ssdmfun  6841  dffo4  6868  dffo5  6869  funopsn  6909  fvclss  7000  fsnex  7038  f1prex  7039  f1eqcocnv  7056  mapsnd  8449  enp1i  8752  en2  8753  en4  8755  marypha2  8902  brwdom3  9045  isinffi  9420  infpwfien  9487  infmap2  9639  cfub  9670  cflm  9671  cff1  9679  cfss  9686  isf32lem9  9782  axcc4  9860  acncc  9861  domtriomlem  9863  ac6s  9905  iundom2g  9961  winalim2  10117  grudomon  10238  nsmallnq  10398  prnmadd  10418  ltexprlem1  10457  ltexprlem3  10459  ltexprlem4  10460  reclem2pr  10469  dedekind  10802  xrsupsslem  12699  xrinfmsslem  12700  ishashinf  13820  coss12d  14331  supcvg  15210  vdwlem2  16317  ram0  16357  mreexexlem2d  16915  initoeu1  17270  termoeu1  17277  acsmapd  17787  acsmap2d  17788  dirge  17846  odcau  18728  ablfac2  19210  lspprat  19924  cmpsub  22007  cmpcld  22009  2ndcsep  22066  1stcelcls  22068  txcn  22233  fgcl  22485  ufildom1  22533  metustexhalf  23165  bcthlem5  23930  mbfi1flim  24323  itg2seq  24342  dchrisumlem3  26066  upgrex  26876  uhgrvd00  27315  wlkiswwlksupgr2  27654  wlklnwwlkln2lem  27659  umgrwwlks2on  27735  wpthswwlks2on  27739  frcond3  28047  frgrncvvdeqlem9  28085  ubthlem1  28646  axhcompl-zf  28774  isch3  29017  cnlnssadj  29856  acunirnmpt  30403  f1ocnt  30524  qsxpid  30927  insiga  31396  bnj605  32179  bnj607  32188  bnj1018g  32235  bnj1018  32236  cusgredgex  32368  loop1cycl  32384  erdsze2lem1  32450  fundmpss  33009  bj-zfauscl  34243  bj-restn0  34380  dissneqlem  34620  relowlpssretop  34644  pibt2  34697  poimirlem30  34921  fdc1  35020  prdstotbnd  35071  cossss  35669  prter2  36016  lsat0cv  36168  pmapglb2N  36906  elpaddn0  36935  cdlemftr3  37700  dibglbN  38301  dihglbcpreN  38435  dihjatcclem4  38556  mapdordlem2  38772  sn-axprlem3  39107  sn-dtru  39109  dfac11  39660  neik0pk1imk0  40395  rr-spce  40555  cpcolld  40592  ax6e2ndeq  40891  fnchoice  41284  rfcnnnub  41291  eliin2f  41368  founiiun0  41449  axccd  41493  axccd2  41494  fvelima2  41530  fzisoeu  41565  islpcn  41918  lptre2pt  41919  stoweidlem14  42298  stoweidlem35  42319  stoweidlem39  42323  stoweidlem50  42334  stoweidlem56  42340  stoweidlem59  42343  stoweidlem60  42344  fourier2  42511  qndenserrnbllem  42578  qndenserrn  42583  ovncvrrp  42845  ovnsubaddlem2  42852  hoidmvval0b  42871  hoiqssbllem3  42905  funressnfv  43277  imasetpreimafvbijlemfv1  43562  fundcmpsurinjpreimafv  43567  elsprel  43636