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

Theorem eximdv 1911
Description: Deduction form of Theorem 19.22 of [Margaris] p. 90, see exim 1827. See eximdh 1858 and eximd 2209 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 1904 . 2 (𝜑 → ∀𝑥𝜑)
2 alimdv.1 . 2 (𝜑 → (𝜓𝜒))
31, 2eximdh 1858 1 (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1773
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904
This theorem depends on definitions:  df-bi 208  df-ex 1774
This theorem is referenced by:  2eximdv  1913  exlimdv  1927  19.41v  1943  equvinva  2030  sbimdvOLD  2514  dfmoeu  2615  moim  2623  mo4  2647  reximdv2  3275  cgsexg  3542  spcimdv  3596  spcegv  3601  euind  3718  ssel  3964  reupick  4290  reximdva0  4315  uniss  4857  eusvnfb  5289  reusv2lem3  5296  axprlem1  5319  axprlem2  5320  axprlem3  5321  axpr  5324  relopabi  5692  coss1  5724  coss2  5725  ssrelrn  5761  dmss  5769  dmcosseq  5842  funssres  6394  brprcneu  6658  fv3  6684  dffv2  6752  fvn0ssdmfun  6837  dffo4  6864  dffo5  6865  funopsn  6905  fvclss  6998  fsnex  7036  f1prex  7037  f1eqcocnv  7054  mapsnd  8442  enp1i  8745  en2  8746  en4  8748  marypha2  8895  brwdom3  9038  isinffi  9413  infpwfien  9480  infmap2  9632  cfub  9663  cflm  9664  cff1  9672  cfss  9679  isf32lem9  9775  axcc4  9853  acncc  9854  domtriomlem  9856  ac6s  9898  iundom2g  9954  winalim2  10110  grudomon  10231  nsmallnq  10391  prnmadd  10411  ltexprlem1  10450  ltexprlem3  10452  ltexprlem4  10453  reclem2pr  10462  dedekind  10795  xrsupsslem  12693  xrinfmsslem  12694  ishashinf  13814  coss12d  14325  supcvg  15203  vdwlem2  16310  ram0  16350  mreexexlem2d  16908  initoeu1  17263  termoeu1  17270  acsmapd  17780  acsmap2d  17781  dirge  17839  odcau  18651  ablfac2  19133  lspprat  19847  cmpsub  21924  cmpcld  21926  2ndcsep  21983  1stcelcls  21985  txcn  22150  fgcl  22402  ufildom1  22450  metustexhalf  23081  bcthlem5  23846  mbfi1flim  24239  itg2seq  24258  dchrisumlem3  25981  upgrex  26791  uhgrvd00  27230  wlkiswwlksupgr2  27569  wlklnwwlkln2lem  27574  umgrwwlks2on  27650  wpthswwlks2on  27654  frcond3  27962  frgrncvvdeqlem9  28000  ubthlem1  28561  axhcompl-zf  28689  isch3  28932  cnlnssadj  29771  acunirnmpt  30319  f1ocnt  30438  qsxpid  30841  insiga  31282  bnj605  32065  bnj607  32074  bnj1018  32120  cusgredgex  32252  loop1cycl  32268  erdsze2lem1  32334  fundmpss  32893  bj-zfauscl  34127  bj-restn0  34262  dissneqlem  34490  relowlpssretop  34514  pibt2  34567  poimirlem30  34789  fdc1  34889  prdstotbnd  34940  cossss  35537  prter2  35884  lsat0cv  36036  pmapglb2N  36774  elpaddn0  36803  cdlemftr3  37568  dibglbN  38169  dihglbcpreN  38303  dihjatcclem4  38424  mapdordlem2  38640  sn-axprlem3  38974  sn-dtru  38976  dfac11  39523  neik0pk1imk0  40258  rr-spce  40419  cpcolld  40455  ax6e2ndeq  40754  fnchoice  41147  rfcnnnub  41154  eliin2f  41232  founiiun0  41312  axccd  41356  axccd2  41357  fvelima2  41393  fzisoeu  41428  islpcn  41781  lptre2pt  41782  stoweidlem14  42161  stoweidlem35  42182  stoweidlem39  42186  stoweidlem50  42197  stoweidlem56  42203  stoweidlem59  42206  stoweidlem60  42207  fourier2  42374  qndenserrnbllem  42441  qndenserrn  42446  ovncvrrp  42708  ovnsubaddlem2  42715  hoidmvval0b  42734  hoiqssbllem3  42768  funressnfv  43140  elsprel  43465
  Copyright terms: Public domain W3C validator