Theorem eximdv 1917

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

Syntax hints:   → wi 4  ∃wex 1779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-ex 1780

This theorem is referenced by:  2eximdv  1919  exlimdv  1933  19.41v  1949  equvinva  2030  dfmoeu  2529  moim  2537  mo4  2559  reximdv2  3143  cgsexg  3492  spcimdv  3559  spcegv  3563  euind  3695  sbcimdv  3822  reupick  4292  reximdva0  4318  uniss  4879  dfiun2g  4994  sepexlem  5254  eusvnfb  5348  reusv2lem3  5355  axprlem1  5378  axprlem2  5379  axprlem4  5381  axpr  5382  axprlem3OLD  5383  axprOLD  5386  exexneq  5394  relopabi  5785  coss1  5819  coss2  5820  ssrelrn  5858  dmss  5866  dmcosseq  5940  dmcosseqOLD  5941  funssres  6560  brprcneu  6848  brprcneuALT  6849  fv3  6876  fvelima2  6913  dffv2  6956  fvn0ssdmfun  7046  dffo4  7075  dffo5  7076  funopsn  7120  fvclss  7215  fsnex  7258  f1prex  7259  f1eqcocnv  7276  mapsnd  8859  enp1iOLD  9225  en2  9226  en4  9228  marypha2  9390  brwdom3  9535  isinffi  9945  infpwfien  10015  infmap2  10170  cfub  10202  cflm  10203  cff1  10211  cfss  10218  isf32lem9  10314  axcc4  10392  acncc  10393  domtriomlem  10395  ac6s  10437  iundom2g  10493  winalim2  10649  grudomon  10770  nsmallnq  10930  prnmadd  10950  ltexprlem1  10989  ltexprlem3  10991  ltexprlem4  10992  reclem2pr  11001  dedekind  11337  xrsupsslem  13267  xrinfmsslem  13268  ishashinf  14428  hash3tpde  14458  coss12d  14938  supcvg  15822  vdwlem2  16953  ram0  16993  mreexexlem2d  17606  initoeu1  17973  termoeu1  17980  acsmapd  18513  acsmap2d  18514  dirge  18562  odcau  19534  ablfac2  20021  lspprat  21063  cmpsub  23287  cmpcld  23289  2ndcsep  23346  1stcelcls  23348  txcn  23513  fgcl  23765  ufildom1  23813  metustexhalf  24444  bcthlem5  25228  mbfi1flim  25624  itg2seq  25643  dchrisumlem3  27402  upgrex  29019  uhgrvd00  29462  wlkiswwlksupgr2  29807  wlklnwwlkln2lem  29812  umgrwwlks2on  29887  wpthswwlks2on  29891  frcond3  30198  frgrncvvdeqlem9  30236  ubthlem1  30799  axhcompl-zf  30927  isch3  31170  cnlnssadj  32009  ac6mapd  32549  acunirnmpt  32583  f1ocnt  32725  wrdpmtrlast  33050  qsxpid  33333  zarclsint  33862  insiga  34127  bnj605  34897  bnj607  34906  bnj1018g  34953  bnj1018  34954  cusgredgex  35109  loop1cycl  35124  erdsze2lem1  35190  fundmpss  35754  bj-zfauscl  36912  bj-restn0  37078  dissneqlem  37328  relowlpssretop  37352  pibt2  37405  wl-isseteq  37493  poimirlem30  37644  fdc1  37740  prdstotbnd  37788  cossss  38416  prter2  38874  lsat0cv  39026  pmapglb2N  39765  elpaddn0  39794  cdlemftr3  40559  dibglbN  41160  dihglbcpreN  41294  dihjatcclem4  41415  mapdordlem2  41631  sticksstones3  42136  sticksstones20  42154  sn-axprlem3  42205  eu6w  42664  dfac11  43051  neik0pk1imk0  44036  rr-spce  44193  cpcolld  44247  ismnushort  44290  ax6e2ndeq  44549  ssclaxsep  44972  fnchoice  45023  rfcnnnub  45030  eliin2f  45098  founiiun0  45184  disjinfi  45186  axccd  45223  axccd2  45224  fzisoeu  45298  islpcn  45637  lptre2pt  45638  stoweidlem14  46012  stoweidlem35  46033  stoweidlem39  46037  stoweidlem50  46048  stoweidlem56  46054  stoweidlem59  46057  stoweidlem60  46058  fourier2  46225  qndenserrnbllem  46292  qndenserrn  46297  ovncvrrp  46562  ovnsubaddlem2  46569  hoidmvval0b  46588  hoiqssbllem3  46622  ormklocald  46872  natlocalincr  46874  tworepnotupword  46884  funressnfv  47044  imasetpreimafvbijlemfv1  47404  fundcmpsurinjpreimafv  47409  elsprel  47476  isubgredg  47866  isubgr3stgr  47974  grilcbri2  48003  clnbgr3stgrgrlic  48011  subthinc  49432