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  2553  moim  2561  mo4  2584  reximdv2  3195  cgsexg  3455  spcimdv  3512  spcegv  3517  euind  3640  sselOLD  3888  reupick  4223  reximdva0  4252  uniss  4809  eusvnfb  5265  reusv2lem3  5272  axprlem1  5295  axprlem2  5296  axprlem3  5297  axpr  5300  relopabi  5668  coss1  5700  coss2  5701  ssrelrn  5739  dmss  5747  dmcosseq  5818  funssres  6383  brprcneu  6653  fvprc  6654  fv3  6680  dffv2  6751  fvn0ssdmfun  6838  dffo4  6865  dffo5  6866  funopsn  6906  fvclss  6998  fsnex  7036  f1prex  7037  f1eqcocnv  7054  f1eqcocnvOLD  7055  mapsnd  8473  enp1i  8794  en2  8795  en4  8797  marypha2  8941  brwdom3  9084  isinffi  9459  infpwfien  9527  infmap2  9683  cfub  9714  cflm  9715  cff1  9723  cfss  9730  isf32lem9  9826  axcc4  9904  acncc  9905  domtriomlem  9907  ac6s  9949  iundom2g  10005  winalim2  10161  grudomon  10282  nsmallnq  10442  prnmadd  10462  ltexprlem1  10501  ltexprlem3  10503  ltexprlem4  10504  reclem2pr  10513  dedekind  10846  xrsupsslem  12746  xrinfmsslem  12747  ishashinf  13878  coss12d  14384  supcvg  15264  vdwlem2  16378  ram0  16418  mreexexlem2d  16979  initoeu1  17342  termoeu1  17349  acsmapd  17859  acsmap2d  17860  dirge  17918  odcau  18801  ablfac2  19284  lspprat  19998  cmpsub  22105  cmpcld  22107  2ndcsep  22164  1stcelcls  22166  txcn  22331  fgcl  22583  ufildom1  22631  metustexhalf  23263  bcthlem5  24033  mbfi1flim  24428  itg2seq  24447  dchrisumlem3  26179  upgrex  26989  uhgrvd00  27428  wlkiswwlksupgr2  27767  wlklnwwlkln2lem  27772  umgrwwlks2on  27847  wpthswwlks2on  27851  frcond3  28158  frgrncvvdeqlem9  28196  ubthlem1  28757  axhcompl-zf  28885  isch3  29128  cnlnssadj  29967  acunirnmpt  30524  f1ocnt  30651  qsxpid  31083  zarclsint  31347  insiga  31628  bnj605  32411  bnj607  32420  bnj1018g  32467  bnj1018  32468  cusgredgex  32603  loop1cycl  32619  erdsze2lem1  32685  fundmpss  33260  bj-zfauscl  34674  bj-restn0  34811  dissneqlem  35063  relowlpssretop  35087  pibt2  35140  poimirlem30  35393  fdc1  35490  prdstotbnd  35538  cossss  36136  prter2  36483  lsat0cv  36635  pmapglb2N  37373  elpaddn0  37402  cdlemftr3  38167  dibglbN  38768  dihglbcpreN  38902  dihjatcclem4  39023  mapdordlem2  39239  sn-axprlem3  39729  sn-dtru  39731  dfac11  40407  neik0pk1imk0  41151  rr-spce  41311  cpcolld  41367  ax6e2ndeq  41666  fnchoice  42059  rfcnnnub  42066  eliin2f  42141  founiiun0  42215  disjinfi  42218  axccd  42257  axccd2  42258  fvelima2  42294  fzisoeu  42328  islpcn  42675  lptre2pt  42676  stoweidlem14  43050  stoweidlem35  43071  stoweidlem39  43075  stoweidlem50  43086  stoweidlem56  43092  stoweidlem59  43095  stoweidlem60  43096  fourier2  43263  qndenserrnbllem  43330  qndenserrn  43335  ovncvrrp  43597  ovnsubaddlem2  43604  hoidmvval0b  43623  hoiqssbllem3  43657  funressnfv  44029  imasetpreimafvbijlemfv1  44316  fundcmpsurinjpreimafv  44321  elsprel  44388