MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eximdv Structured version   Visualization version   GIF version

Theorem eximdv 2008
Description: Deduction form of Theorem 19.22 of [Margaris] p. 90, see exim 1918. (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
StepHypRef Expression
1 ax-5 2001 . 2 (𝜑 → ∀𝑥𝜑)
2 alimdv.1 . 2 (𝜑 → (𝜓𝜒))
31, 2eximdh 1952 1 (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1859
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001
This theorem depends on definitions:  df-bi 198  df-ex 1860
This theorem is referenced by:  2eximdv  2010  exlimdv  2024  19.41v  2040  19.41vOLD  2093  equvinvOLD  2127  equvinva  2128  mo2v  2637  moim  2680  reximdv2  3199  cgsexg  3430  spc3egv  3488  euind  3589  ssel  3790  reupick  4110  reximdva0  4132  uniss  4651  eusvnfb  5060  reusv2lem3  5067  relopabi  5445  coss1  5477  coss2  5478  ssrelrn  5514  dmss  5522  dmcosseq  5586  funssres  6142  brprcneu  6398  fv3  6424  dffv2  6490  fvn0ssdmfun  6570  dffo4  6595  dffo5  6596  funopsn  6635  fvclss  6722  fsnex  6760  f1prex  6761  f1eqcocnv  6778  mapsnd  8132  enp1i  8432  en2  8433  en4  8435  marypha2  8582  brwdom3  8724  isinffi  9099  infpwfien  9166  infmap2  9323  cfub  9354  cflm  9355  cff1  9363  cfss  9370  isf32lem9  9466  axcc4  9544  acncc  9545  domtriomlem  9547  ac6s  9589  iundom2g  9645  winalim2  9801  grudomon  9922  nsmallnq  10082  prnmadd  10102  ltexprlem1  10141  ltexprlem3  10143  ltexprlem4  10144  reclem2pr  10153  dedekind  10483  xrsupsslem  12353  xrinfmsslem  12354  ishashinf  13462  coss12d  13934  supcvg  14808  vdwlem2  15901  ram0  15941  mreexexlem2d  16508  initoeu1  16863  termoeu1  16870  acsmapd  17381  acsmap2d  17382  dirge  17440  odcau  18218  ablfac2  18688  lspprat  19360  cmpsub  21415  cmpcld  21417  2ndcsep  21474  1stcelcls  21476  txcn  21641  fgcl  21893  ufildom1  21941  metustexhalf  22572  bcthlem5  23335  mbfi1flim  23702  itg2seq  23721  dchrisumlem3  25392  upgrex  26199  uhgrvd00  26656  wlkiswwlksupgr2  27002  wlklnwwlkln2lem  27007  umgrwwlks2on  27096  wpthswwlks2on  27100  wpthswwlks2onOLD  27101  frcond3  27442  frgrncvvdeqlem9  27480  ubthlem1  28052  axhcompl-zf  28181  isch3  28424  cnlnssadj  29265  acunirnmpt  29784  f1ocnt  29884  insiga  30523  bnj605  31298  bnj607  31307  bnj1018  31353  erdsze2lem1  31506  fundmpss  31984  bj-zfauscl  33230  bj-restn0  33352  dissneqlem  33502  relowlpssretop  33526  poimirlem30  33750  fdc1  33851  prdstotbnd  33902  cossss  34491  prter2  34658  lsat0cv  34811  pmapglb2N  35549  elpaddn0  35578  cdlemftr3  36344  dibglbN  36945  dihglbcpreN  37079  dihjatcclem4  37200  mapdordlem2  37416  dfac11  38131  neik0pk1imk0  38843  ax6e2ndeq  39271  fnchoice  39680  rfcnnnub  39687  eliin2f  39777  founiiun0  39864  axccd  39911  axccd2  39912  fvelima2  39956  fzisoeu  39993  islpcn  40349  lptre2pt  40350  stoweidlem14  40708  stoweidlem35  40729  stoweidlem39  40733  stoweidlem50  40744  stoweidlem56  40750  stoweidlem59  40753  stoweidlem60  40754  fourier2  40921  qndenserrnbllem  40991  qndenserrn  40996  ovncvrrp  41258  ovnsubaddlem2  41265  hoidmvval0b  41284  hoiqssbllem3  41318  funressnfv  41660  elsprel  42291
  Copyright terms: Public domain W3C validator