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

Theorem eximdv 1920
Description: Deduction form of Theorem 19.22 of [Margaris] p. 90, see exim 1836. See eximdh 1867 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 1913 . 2 (𝜑 → ∀𝑥𝜑)
2 alimdv.1 . 2 (𝜑 → (𝜓𝜒))
31, 2eximdh 1867 1 (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1781
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913
This theorem depends on definitions:  df-bi 206  df-ex 1782
This theorem is referenced by:  2eximdv  1922  exlimdv  1936  19.41v  1953  equvinva  2033  dfmoeu  2534  moim  2542  mo4  2564  reximdv2  3159  cgsexg  3486  spcimdv  3550  spcegv  3554  euind  3680  sbcimdv  3811  sselOLD  3936  reupick  4276  reximdva0  4309  uniss  4871  dfiun2g  4988  eusvnfb  5346  reusv2lem3  5353  axprlem1  5376  axprlem2  5377  axprlem3  5378  axpr  5381  exexneq  5389  relopabi  5776  coss1  5809  coss2  5810  ssrelrn  5848  dmss  5856  dmcosseq  5926  funssres  6542  brprcneu  6829  brprcneuALT  6830  fv3  6857  dffv2  6933  fvn0ssdmfun  7022  dffo4  7049  dffo5  7050  funopsn  7090  fvclss  7185  fsnex  7225  f1prex  7226  f1eqcocnv  7243  f1eqcocnvOLD  7244  mapsnd  8820  enp1iOLD  9220  en2  9221  en4  9223  marypha2  9371  brwdom3  9514  isinffi  9924  infpwfien  9994  infmap2  10150  cfub  10181  cflm  10182  cff1  10190  cfss  10197  isf32lem9  10293  axcc4  10371  acncc  10372  domtriomlem  10374  ac6s  10416  iundom2g  10472  winalim2  10628  grudomon  10749  nsmallnq  10909  prnmadd  10929  ltexprlem1  10968  ltexprlem3  10970  ltexprlem4  10971  reclem2pr  10980  dedekind  11314  xrsupsslem  13218  xrinfmsslem  13219  ishashinf  14354  coss12d  14849  supcvg  15733  vdwlem2  16846  ram0  16886  mreexexlem2d  17517  initoeu1  17889  termoeu1  17896  acsmapd  18435  acsmap2d  18436  dirge  18484  odcau  19377  ablfac2  19859  lspprat  20599  cmpsub  22735  cmpcld  22737  2ndcsep  22794  1stcelcls  22796  txcn  22961  fgcl  23213  ufildom1  23261  metustexhalf  23896  bcthlem5  24676  mbfi1flim  25072  itg2seq  25091  dchrisumlem3  26823  upgrex  27929  uhgrvd00  28368  wlkiswwlksupgr2  28708  wlklnwwlkln2lem  28713  umgrwwlks2on  28788  wpthswwlks2on  28792  frcond3  29099  frgrncvvdeqlem9  29137  ubthlem1  29698  axhcompl-zf  29826  isch3  30069  cnlnssadj  30908  acunirnmpt  31461  f1ocnt  31588  qsxpid  32033  zarclsint  32322  insiga  32605  bnj605  33388  bnj607  33397  bnj1018g  33444  bnj1018  33445  cusgredgex  33584  loop1cycl  33600  erdsze2lem1  33666  fundmpss  34211  bj-zfauscl  35361  bj-restn0  35528  dissneqlem  35778  relowlpssretop  35802  pibt2  35855  poimirlem30  36075  fdc1  36172  prdstotbnd  36220  cossss  36854  prter2  37310  lsat0cv  37462  pmapglb2N  38201  elpaddn0  38230  cdlemftr3  38995  dibglbN  39596  dihglbcpreN  39730  dihjatcclem4  39851  mapdordlem2  40067  sticksstones3  40523  sticksstones20  40541  sn-axprlem3  40605  dfac11  41327  neik0pk1imk0  42261  rr-spce  42419  cpcolld  42480  ismnushort  42523  ax6e2ndeq  42783  fnchoice  43176  rfcnnnub  43183  eliin2f  43256  founiiun0  43345  disjinfi  43348  axccd  43386  axccd2  43387  fvelima2  43424  fzisoeu  43470  islpcn  43812  lptre2pt  43813  stoweidlem14  44187  stoweidlem35  44208  stoweidlem39  44212  stoweidlem50  44223  stoweidlem56  44229  stoweidlem59  44232  stoweidlem60  44233  fourier2  44400  qndenserrnbllem  44467  qndenserrn  44472  ovncvrrp  44737  ovnsubaddlem2  44744  hoidmvval0b  44763  hoiqssbllem3  44797  natlocalincr  45047  tworepnotupword  45057  funressnfv  45209  imasetpreimafvbijlemfv1  45527  fundcmpsurinjpreimafv  45532  elsprel  45599  subthinc  46992
  Copyright terms: Public domain W3C validator