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

Theorem eximdv 1843
Description: Deduction form of Theorem 19.22 of [Margaris] p. 90, see exim 1758. (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 1836 . 2 (𝜑 → ∀𝑥𝜑)
2 alimdv.1 . 2 (𝜑 → (𝜓𝜒))
31, 2eximdh 1788 1 (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1701
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836
This theorem depends on definitions:  df-bi 197  df-ex 1702
This theorem is referenced by:  2eximdv  1845  exlimdv  1858  19.41v  1911  equvinv  1956  equviniva  1957  equvinivOLD  1958  mo2v  2476  moim  2518  reximdv2  3009  cgsexg  3227  spc3egv  3286  euind  3379  ssel  3581  reupick  3892  reximdva0  3914  uniss  4429  eusvnfb  4827  reusv2lem3  4836  relopabi  5210  coss1  5242  coss2  5243  ssrelrn  5280  dmss  5288  dmcosseq  5352  funssres  5893  brprcneu  6146  fv3  6168  dffv2  6233  fvn0ssdmfun  6311  dffo4  6336  dffo5  6337  funopsn  6373  fvclss  6460  fsnex  6498  f1prex  6499  f1eqcocnv  6516  mapsn  7851  enp1i  8147  en2  8148  en4  8150  marypha2  8297  brwdom3  8439  isinffi  8770  infpwfien  8837  infmap2  8992  cfub  9023  cflm  9024  cff1  9032  cfss  9039  isf32lem9  9135  axcc4  9213  acncc  9214  domtriomlem  9216  ac6s  9258  iundom2g  9314  winalim2  9470  grudomon  9591  nsmallnq  9751  prnmadd  9771  ltexprlem1  9810  ltexprlem3  9812  ltexprlem4  9813  reclem2pr  9822  dedekind  10152  xrsupsslem  12088  xrinfmsslem  12089  ishashinf  13193  coss12d  13653  supcvg  14524  vdwlem2  15621  ram0  15661  mreexexlem2d  16237  initoeu1  16593  termoeu1  16600  acsmapd  17110  acsmap2d  17111  dirge  17169  odcau  17951  ablfac2  18420  lspprat  19085  cmpsub  21126  cmpcld  21128  2ndcsep  21185  1stcelcls  21187  txcn  21352  fgcl  21605  ufildom1  21653  metustexhalf  22284  bcthlem5  23048  mbfi1flim  23413  itg2seq  23432  dchrisumlem3  25097  upgrex  25900  uhgrvd00  26333  wlkiswwlksupgr2  26649  wlklnwwlkln2lem  26654  umgrwwlks2on  26736  wpthswwlks2on  26739  frcond3  27015  frgrncvvdeqlemC  27053  ubthlem1  27596  axhcompl-zf  27725  isch3  27968  cnlnssadj  28809  acunirnmpt  29324  f1ocnt  29424  insiga  30005  bnj605  30720  bnj607  30729  bnj1018  30775  erdsze2lem1  30928  fundmpss  31403  bj-restn0  32715  dissneqlem  32854  relowlpssretop  32879  poimirlem30  33106  fdc1  33209  prdstotbnd  33260  prter2  33681  lsat0cv  33835  pmapglb2N  34572  elpaddn0  34601  cdlemftr3  35368  dibglbN  35970  dihglbcpreN  36104  dihjatcclem4  36225  mapdordlem2  36441  dfac11  37147  neik0pk1imk0  37862  ax6e2ndeq  38292  fnchoice  38706  rfcnnnub  38713  eliin2f  38805  founiiun0  38882  mapsnd  38893  axccd  38934  axccd2  38935  fzisoeu  39009  islpcn  39303  lptre2pt  39304  stoweidlem14  39564  stoweidlem35  39585  stoweidlem39  39589  stoweidlem50  39600  stoweidlem56  39606  stoweidlem59  39609  stoweidlem60  39610  fourier2  39777  qndenserrnbllem  39847  qndenserrn  39852  ovncvrrp  40111  ovnsubaddlem2  40118  hoidmvval0b  40137  hoiqssbllem3  40171  funressnfv  40538  elsprel  41039
  Copyright terms: Public domain W3C validator