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

Theorem eximi 1910
Description: Inference adding existential quantifier to antecedent and consequent. (Contributed by NM, 10-Jan-1993.)
Hypothesis
Ref Expression
eximi.1 (𝜑𝜓)
Assertion
Ref Expression
eximi (∃𝑥𝜑 → ∃𝑥𝜓)

Proof of Theorem eximi
StepHypRef Expression
1 exim 1909 . 2 (∀𝑥(𝜑𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))
2 eximi.1 . 2 (𝜑𝜓)
31, 2mpg 1872 1 (∃𝑥𝜑 → ∃𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1852
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885
This theorem depends on definitions:  df-bi 197  df-ex 1853
This theorem is referenced by:  2eximi  1911  eximii  1912  exa1  1913  exan  1939  exsimpl  1946  exsimpr  1947  19.29r2  1955  19.29x  1956  19.35  1957  19.40-2  1966  exlimiv  2010  speimfwALT  2046  sbimi  2055  19.12  2326  ax13lem2  2451  exdistrf  2483  equs45f  2496  mo2v  2625  2eu2ex  2695  reximi2  3158  cgsexg  3390  gencbvex  3402  vtocl3  3414  eqvincg  3480  n0rex  4083  axrep2  4908  bm1.3ii  4919  ax6vsep  4920  copsexg  5084  relopabi  5385  dminss  5689  imainss  5690  iotaex  6012  fv3  6348  ssimaex  6406  dffv2  6414  exfo  6521  oprabid  6823  zfrep6  7282  frxp  7439  suppimacnvss  7457  tz7.48-1  7692  enssdom  8135  fineqvlem  8331  infcntss  8391  infeq5  8699  omex  8705  rankuni  8891  scott0  8914  acni3  9071  acnnum  9076  dfac3  9145  dfac9  9161  kmlem1  9175  cflm  9275  cfcof  9299  axdc4lem  9480  axcclem  9482  ac6c4  9506  ac6s  9509  ac6s2  9511  axdclem2  9545  brdom3  9553  brdom5  9554  brdom4  9555  nqpr  10039  ltexprlem4  10064  reclem2pr  10073  hash1to3  13476  trclublem  13945  drsdirfi  17147  toprntopon  20951  2ndcsb  21474  fbssint  21863  isfil2  21881  alexsubALTlem3  22074  lpbl  22529  metustfbas  22583  ex-natded9.26-2  27620  19.9d2rf  29659  rexunirn  29671  f1ocnt  29900  fsumiunle  29916  fmcncfil  30318  esumiun  30497  0elsiga  30518  ddemeas  30640  bnj168  31137  bnj593  31154  bnj607  31325  bnj600  31328  bnj916  31342  fundmpss  32003  exisym1  32761  bj-exlime  32947  bj-sbex  32965  bj-ssbequ2  32981  bj-equs45fv  33089  bj-axrep2  33126  bj-eumo0  33166  bj-snsetex  33283  bj-snglss  33290  bj-snglex  33293  bj-bm1.3ii  33356  bj-restn0  33376  bj-ccinftydisj  33438  mptsnunlem  33523  spsbce-2  39107  iotaexeu  39146  iotasbc  39147  relopabVD  39660  ax6e2ndeqVD  39668  2uasbanhVD  39670  ax6e2ndeqALT  39690  fnchoice  39711  rfcnnnub  39718  stoweidlem35  40770  stoweidlem57  40792
  Copyright terms: Public domain W3C validator