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

Theorem eximdv 1886
Description: Deduction form of Theorem 19.22 of [Margaris] p. 90, see exim 1801. (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 1879 . 2 (𝜑 → ∀𝑥𝜑)
2 alimdv.1 . 2 (𝜑 → (𝜓𝜒))
31, 2eximdh 1831 1 (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1744
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879
This theorem depends on definitions:  df-bi 197  df-ex 1745
This theorem is referenced by:  2eximdv  1888  exlimdv  1901  19.41v  1917  19.41vOLD  1970  equvinv  2003  equviniva  2004  mo2v  2505  moim  2548  reximdv2  3043  cgsexg  3269  spc3egv  3328  euind  3426  ssel  3630  reupick  3944  reximdva0  3966  uniss  4490  eusvnfb  4892  reusv2lem3  4901  relopabi  5278  coss1  5310  coss2  5311  ssrelrn  5347  dmss  5355  dmcosseq  5419  funssres  5968  brprcneu  6222  fv3  6244  dffv2  6310  fvn0ssdmfun  6390  dffo4  6415  dffo5  6416  funopsn  6453  fvclss  6540  fsnex  6578  f1prex  6579  f1eqcocnv  6596  mapsn  7941  enp1i  8236  en2  8237  en4  8239  marypha2  8386  brwdom3  8528  isinffi  8856  infpwfien  8923  infmap2  9078  cfub  9109  cflm  9110  cff1  9118  cfss  9125  isf32lem9  9221  axcc4  9299  acncc  9300  domtriomlem  9302  ac6s  9344  iundom2g  9400  winalim2  9556  grudomon  9677  nsmallnq  9837  prnmadd  9857  ltexprlem1  9896  ltexprlem3  9898  ltexprlem4  9899  reclem2pr  9908  dedekind  10238  xrsupsslem  12175  xrinfmsslem  12176  ishashinf  13285  coss12d  13757  supcvg  14632  vdwlem2  15733  ram0  15773  mreexexlem2d  16352  initoeu1  16708  termoeu1  16715  acsmapd  17225  acsmap2d  17226  dirge  17284  odcau  18065  ablfac2  18534  lspprat  19201  cmpsub  21251  cmpcld  21253  2ndcsep  21310  1stcelcls  21312  txcn  21477  fgcl  21729  ufildom1  21777  metustexhalf  22408  bcthlem5  23171  mbfi1flim  23535  itg2seq  23554  dchrisumlem3  25225  upgrex  26032  uhgrvd00  26486  wlkiswwlksupgr2  26831  wlklnwwlkln2lem  26836  umgrwwlks2on  26923  wpthswwlks2on  26927  wpthswwlks2onOLD  26928  frcond3  27249  frgrncvvdeqlem9  27287  ubthlem1  27854  axhcompl-zf  27983  isch3  28226  cnlnssadj  29067  acunirnmpt  29587  f1ocnt  29687  insiga  30328  bnj605  31103  bnj607  31112  bnj1018  31158  erdsze2lem1  31311  fundmpss  31790  bj-restn0  33168  dissneqlem  33317  relowlpssretop  33342  poimirlem30  33569  fdc1  33672  prdstotbnd  33723  cossss  34320  prter2  34485  lsat0cv  34638  pmapglb2N  35375  elpaddn0  35404  cdlemftr3  36170  dibglbN  36772  dihglbcpreN  36906  dihjatcclem4  37027  mapdordlem2  37243  dfac11  37949  neik0pk1imk0  38662  ax6e2ndeq  39092  fnchoice  39502  rfcnnnub  39509  eliin2f  39601  founiiun0  39691  mapsnd  39702  axccd  39743  axccd2  39744  fvelima2  39789  fzisoeu  39828  islpcn  40189  lptre2pt  40190  stoweidlem14  40549  stoweidlem35  40570  stoweidlem39  40574  stoweidlem50  40585  stoweidlem56  40591  stoweidlem59  40594  stoweidlem60  40595  fourier2  40762  qndenserrnbllem  40832  qndenserrn  40837  ovncvrrp  41099  ovnsubaddlem2  41106  hoidmvval0b  41125  hoiqssbllem3  41159  funressnfv  41529  elsprel  42050
  Copyright terms: Public domain W3C validator