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

Theorem eximdv 1921
Description: Deduction form of Theorem 19.22 of [Margaris] p. 90, see exim 1837. See eximdh 1868 and eximd 2210 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 1914 . 2 (𝜑 → ∀𝑥𝜑)
2 alimdv.1 . 2 (𝜑 → (𝜓𝜒))
31, 2eximdh 1868 1 (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1782
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914
This theorem depends on definitions:  df-bi 206  df-ex 1783
This theorem is referenced by:  2eximdv  1923  exlimdv  1937  19.41v  1954  equvinva  2034  dfmoeu  2535  moim  2543  mo4  2565  reximdv2  3162  cgsexg  3491  spcimdv  3555  spcegv  3559  euind  3687  sbcimdv  3818  sselOLD  3943  reupick  4283  reximdva0  4316  uniss  4878  dfiun2g  4995  eusvnfb  5353  reusv2lem3  5360  axprlem1  5383  axprlem2  5384  axprlem3  5385  axpr  5388  exexneq  5396  relopabi  5783  coss1  5816  coss2  5817  ssrelrn  5855  dmss  5863  dmcosseq  5933  funssres  6550  brprcneu  6837  brprcneuALT  6838  fv3  6865  dffv2  6941  fvn0ssdmfun  7030  dffo4  7058  dffo5  7059  funopsn  7099  fvclss  7194  fsnex  7234  f1prex  7235  f1eqcocnv  7252  f1eqcocnvOLD  7253  mapsnd  8831  enp1iOLD  9231  en2  9232  en4  9234  marypha2  9382  brwdom3  9525  isinffi  9935  infpwfien  10005  infmap2  10161  cfub  10192  cflm  10193  cff1  10201  cfss  10208  isf32lem9  10304  axcc4  10382  acncc  10383  domtriomlem  10385  ac6s  10427  iundom2g  10483  winalim2  10639  grudomon  10760  nsmallnq  10920  prnmadd  10940  ltexprlem1  10979  ltexprlem3  10981  ltexprlem4  10982  reclem2pr  10991  dedekind  11325  xrsupsslem  13233  xrinfmsslem  13234  ishashinf  14369  coss12d  14864  supcvg  15748  vdwlem2  16861  ram0  16901  mreexexlem2d  17532  initoeu1  17904  termoeu1  17911  acsmapd  18450  acsmap2d  18451  dirge  18499  odcau  19393  ablfac2  19875  lspprat  20630  cmpsub  22767  cmpcld  22769  2ndcsep  22826  1stcelcls  22828  txcn  22993  fgcl  23245  ufildom1  23293  metustexhalf  23928  bcthlem5  24708  mbfi1flim  25104  itg2seq  25123  dchrisumlem3  26855  upgrex  28085  uhgrvd00  28524  wlkiswwlksupgr2  28864  wlklnwwlkln2lem  28869  umgrwwlks2on  28944  wpthswwlks2on  28948  frcond3  29255  frgrncvvdeqlem9  29293  ubthlem1  29854  axhcompl-zf  29982  isch3  30225  cnlnssadj  31064  acunirnmpt  31617  f1ocnt  31747  qsxpid  32190  zarclsint  32493  insiga  32776  bnj605  33559  bnj607  33568  bnj1018g  33615  bnj1018  33616  cusgredgex  33755  loop1cycl  33771  erdsze2lem1  33837  fundmpss  34380  bj-zfauscl  35423  bj-restn0  35590  dissneqlem  35840  relowlpssretop  35864  pibt2  35917  poimirlem30  36137  fdc1  36234  prdstotbnd  36282  cossss  36916  prter2  37372  lsat0cv  37524  pmapglb2N  38263  elpaddn0  38292  cdlemftr3  39057  dibglbN  39658  dihglbcpreN  39792  dihjatcclem4  39913  mapdordlem2  40129  sticksstones3  40585  sticksstones20  40603  sn-axprlem3  40668  dfac11  41418  neik0pk1imk0  42393  rr-spce  42551  cpcolld  42612  ismnushort  42655  ax6e2ndeq  42915  fnchoice  43308  rfcnnnub  43315  eliin2f  43388  founiiun0  43483  disjinfi  43486  axccd  43524  axccd2  43525  fvelima2  43562  fzisoeu  43608  islpcn  43954  lptre2pt  43955  stoweidlem14  44329  stoweidlem35  44350  stoweidlem39  44354  stoweidlem50  44365  stoweidlem56  44371  stoweidlem59  44374  stoweidlem60  44375  fourier2  44542  qndenserrnbllem  44609  qndenserrn  44614  ovncvrrp  44879  ovnsubaddlem2  44886  hoidmvval0b  44905  hoiqssbllem3  44939  natlocalincr  45189  tworepnotupword  45199  funressnfv  45351  imasetpreimafvbijlemfv1  45669  fundcmpsurinjpreimafv  45674  elsprel  45741  subthinc  47134
  Copyright terms: Public domain W3C validator