Theorem eximdv 1919

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

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

This theorem is referenced by:  2eximdv  1921  exlimdv  1935  19.41v  1951  equvinva  2032  dfmoeu  2536  moim  2545  mo4  2567  reximdv2  3148  cgsexg  3475  spcimdv  3536  spcegv  3540  euind  3671  sbcimdv  3798  reupick  4270  reximdva0  4296  uniss  4859  dfiun2g  4973  replem  5224  sepexlem  5235  eusvnfb  5331  reusv2lem3  5338  axprlem2  5362  axprlem4  5364  axpr  5365  axprlem1OLD  5366  axprlem3OLD  5367  axprOLD  5370  axprglem  5374  exexneq  5383  relopabi  5772  coss1  5805  coss2  5806  ssrelrn  5844  dmss  5852  dmcosseq  5928  dmcosseqOLD  5929  dmcosseqOLDOLD  5930  funssres  6537  brprcneu  6825  brprcneuALT  6826  fv3  6853  fvelima2  6887  dffv2  6930  fvn0ssdmfun  7021  dffo4  7050  dffo5  7051  funopsn  7096  fvclss  7190  fsnex  7232  f1prex  7233  f1eqcocnv  7250  mapsnd  8828  en2  9184  en4  9186  marypha2  9346  brwdom3  9491  elirrv  9506  isinffi  9910  infpwfien  9978  infmap2  10133  cfub  10165  cflm  10166  cff1  10174  cfss  10181  isf32lem9  10277  axcc4  10355  acncc  10356  domtriomlem  10358  ac6s  10400  iundom2g  10456  winalim2  10613  grudomon  10734  nsmallnq  10894  prnmadd  10914  ltexprlem1  10953  ltexprlem3  10955  ltexprlem4  10956  reclem2pr  10965  dedekind  11303  xrsupsslem  13253  xrinfmsslem  13254  ishashinf  14419  hash3tpde  14449  coss12d  14928  supcvg  15815  vdwlem2  16947  ram0  16987  mreexexlem2d  17605  initoeu1  17972  termoeu1  17979  acsmapd  18514  acsmap2d  18515  dirge  18563  odcau  19573  ablfac2  20060  lspprat  21146  cmpsub  23378  cmpcld  23380  2ndcsep  23437  1stcelcls  23439  txcn  23604  fgcl  23856  ufildom1  23904  metustexhalf  24534  bcthlem5  25308  mbfi1flim  25703  itg2seq  25722  dchrisumlem3  27471  upgrex  29178  uhgrvd00  29621  wlkiswwlksupgr2  29963  wlklnwwlkln2lem  29968  usgrwwlks2on  30044  umgrwwlks2on  30045  wpthswwlks2on  30050  frcond3  30357  frgrncvvdeqlem9  30395  ubthlem1  30959  axhcompl-zf  31087  isch3  31330  cnlnssadj  32169  ac6mapd  32714  acunirnmpt  32750  padct  32809  f1ocnt  32891  wrdpmtrlast  33172  qsxpid  33440  zarclsint  34035  insiga  34300  bnj605  35068  bnj607  35077  bnj1018g  35124  bnj1018  35125  axprALT2  35272  cusgredgex  35323  loop1cycl  35338  erdsze2lem1  35404  fundmpss  35968  axtco1from2  36676  regsfromregtco  36739  bj-zfauscl  37250  bj-axseprep  37400  bj-restn0  37421  dissneqlem  37673  relowlpssretop  37697  pibt2  37750  wl-isseteq  37838  wl-dfcleq  37847  poimirlem30  37988  fdc1  38084  prdstotbnd  38132  cossss  38853  prter2  39344  lsat0cv  39496  pmapglb2N  40234  elpaddn0  40263  cdlemftr3  41028  dibglbN  41629  dihglbcpreN  41763  dihjatcclem4  41884  sticksstones3  42604  sticksstones20  42622  sn-axprlem3  42676  eu6w  43126  dfac11  43511  neik0pk1imk0  44495  rr-spce  44652  cpcolld  44706  ismnushort  44749  ax6e2ndeq  45007  ssclaxsep  45430  fnchoice  45481  rfcnnnub  45488  eliin2f  45555  founiiun0  45641  disjinfi  45643  axccd  45679  axccd2  45680  fzisoeu  45754  islpcn  46088  lptre2pt  46089  stoweidlem14  46463  stoweidlem35  46484  stoweidlem39  46488  stoweidlem50  46499  stoweidlem56  46505  stoweidlem59  46508  stoweidlem60  46509  fourier2  46676  qndenserrnbllem  46743  qndenserrn  46748  ovncvrrp  47013  ovnsubaddlem2  47020  hoidmvval0b  47039  hoiqssbllem3  47073  ormklocald  47323  natlocalincr  47325  funressnfv  47506  imasetpreimafvbijlemfv1  47878  fundcmpsurinjpreimafv  47883  elsprel  47950  isubgredg  48357  isubgr3stgr  48466  grlimedgclnbgr  48486  grlimprclnbgredg  48488  grlimpredg  48489  grlimprclnbgrvtx  48490  grilcbri2  48502  clnbgr3stgrgrlic  48511  subthinc  49933