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

Theorem eximdv 1909
Description: Deduction form of Theorem 19.22 of [Margaris] p. 90, see exim 1825. See eximdh 1856 and eximd 2206 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
StepHypRef Expression
1 ax-5 1902 . 2 (𝜑 → ∀𝑥𝜑)
2 alimdv.1 . 2 (𝜑 → (𝜓𝜒))
31, 2eximdh 1856 1 (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1771
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902
This theorem depends on definitions:  df-bi 208  df-ex 1772
This theorem is referenced by:  2eximdv  1911  exlimdv  1925  19.41v  1941  equvinva  2028  sbimdvOLD  2509  dfmoeu  2611  moim  2619  mo4  2643  reximdv2  3268  cgsexg  3535  spcimdv  3589  spcegv  3594  euind  3712  ssel  3958  reupick  4284  reximdva0  4309  uniss  4851  eusvnfb  5284  reusv2lem3  5291  axprlem1  5314  axprlem2  5315  axprlem3  5316  axpr  5319  relopabi  5687  coss1  5719  coss2  5720  ssrelrn  5756  dmss  5764  dmcosseq  5837  funssres  6391  brprcneu  6655  fv3  6681  dffv2  6749  fvn0ssdmfun  6834  dffo4  6861  dffo5  6862  funopsn  6902  fvclss  6992  fsnex  7030  f1prex  7031  f1eqcocnv  7048  mapsnd  8438  enp1i  8741  en2  8742  en4  8744  marypha2  8891  brwdom3  9034  isinffi  9409  infpwfien  9476  infmap2  9628  cfub  9659  cflm  9660  cff1  9668  cfss  9675  isf32lem9  9771  axcc4  9849  acncc  9850  domtriomlem  9852  ac6s  9894  iundom2g  9950  winalim2  10106  grudomon  10227  nsmallnq  10387  prnmadd  10407  ltexprlem1  10446  ltexprlem3  10448  ltexprlem4  10449  reclem2pr  10458  dedekind  10791  xrsupsslem  12688  xrinfmsslem  12689  ishashinf  13809  coss12d  14320  supcvg  15199  vdwlem2  16306  ram0  16346  mreexexlem2d  16904  initoeu1  17259  termoeu1  17266  acsmapd  17776  acsmap2d  17777  dirge  17835  odcau  18658  ablfac2  19140  lspprat  19854  cmpsub  21936  cmpcld  21938  2ndcsep  21995  1stcelcls  21997  txcn  22162  fgcl  22414  ufildom1  22462  metustexhalf  23093  bcthlem5  23858  mbfi1flim  24251  itg2seq  24270  dchrisumlem3  25994  upgrex  26804  uhgrvd00  27243  wlkiswwlksupgr2  27582  wlklnwwlkln2lem  27587  umgrwwlks2on  27663  wpthswwlks2on  27667  frcond3  27975  frgrncvvdeqlem9  28013  ubthlem1  28574  axhcompl-zf  28702  isch3  28945  cnlnssadj  29784  acunirnmpt  30332  f1ocnt  30451  qsxpid  30854  insiga  31295  bnj605  32078  bnj607  32087  bnj1018  32133  cusgredgex  32265  loop1cycl  32281  erdsze2lem1  32347  fundmpss  32906  bj-zfauscl  34140  bj-restn0  34275  dissneqlem  34503  relowlpssretop  34527  pibt2  34580  poimirlem30  34803  fdc1  34902  prdstotbnd  34953  cossss  35550  prter2  35897  lsat0cv  36049  pmapglb2N  36787  elpaddn0  36816  cdlemftr3  37581  dibglbN  38182  dihglbcpreN  38316  dihjatcclem4  38437  mapdordlem2  38653  sn-axprlem3  38987  sn-dtru  38989  dfac11  39540  neik0pk1imk0  40275  rr-spce  40435  cpcolld  40471  ax6e2ndeq  40770  fnchoice  41163  rfcnnnub  41170  eliin2f  41247  founiiun0  41327  axccd  41371  axccd2  41372  fvelima2  41408  fzisoeu  41443  islpcn  41796  lptre2pt  41797  stoweidlem14  42176  stoweidlem35  42197  stoweidlem39  42201  stoweidlem50  42212  stoweidlem56  42218  stoweidlem59  42221  stoweidlem60  42222  fourier2  42389  qndenserrnbllem  42456  qndenserrn  42461  ovncvrrp  42723  ovnsubaddlem2  42730  hoidmvval0b  42749  hoiqssbllem3  42783  funressnfv  43155  imasetpreimafvbijlemfv1  43440  fundcmpsurinjpreimafv  43445  elsprel  43514
  Copyright terms: Public domain W3C validator