Theorem eximi 1837

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

Step	Hyp	Ref	Expression
1		exim 1836	. 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))
2		eximi.1	. 2 ⊢ (𝜑 → 𝜓)
3	1, 2	mpg 1800	1 ⊢ (∃𝑥𝜑 → ∃𝑥𝜓)

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

This theorem depends on definitions:  df-bi 206  df-ex 1783

This theorem is referenced by:  2eximi  1838  eximii  1839  exa1  1840  exsimpl  1871  exsimpr  1872  19.29r2  1878  19.29x  1879  19.35  1880  19.40-2  1890  emptyex  1910  exlimiv  1933  speimfwALT  1968  19.12  2321  ax13lem2  2376  exdistrf  2447  equs45f  2459  dfmoeu  2536  moimi  2545  eu6  2574  2eu2ex  2645  reximi2  3175  cgsexg  3474  gencbvex  3488  eqvincg  3578  sbcg  3795  n0rex  4288  axrep2  5212  bm1.3ii  5226  ax6vsep  5227  copsexgw  5404  copsexg  5405  relopabi  5732  dminss  6056  imainss  6057  iotaex  6413  fv3  6792  ssimaex  6853  dffv2  6863  exfo  6981  oprabidw  7306  oprabid  7307  zfrep6  7797  frxp  7967  suppimacnvss  7989  tz7.48-1  8274  enssdom  8765  enfii  8972  fineqvlem  9037  infcntss  9088  infeq5  9395  omex  9401  rankuni  9621  scott0  9644  acni3  9803  acnnum  9808  dfac3  9877  dfac9  9892  kmlem1  9906  cflm  10006  cfcof  10030  axdc4lem  10211  axcclem  10213  ac6c4  10237  ac6s  10240  ac6s2  10242  axdclem2  10276  brdom3  10284  brdom5  10285  brdom4  10286  nqpr  10770  ltexprlem4  10795  reclem2pr  10804  hash1to3  14205  trclublem  14706  fnpr2ob  17269  drsdirfi  18023  toprntopon  22074  2ndcsb  22600  fbssint  22989  isfil2  23007  alexsubALTlem3  23200  lpbl  23659  metustfbas  23713  ex-natded9.26-2  28784  19.9d2rf  30820  rexunirn  30840  f1ocnt  31123  fsumiunle  31143  fmcncfil  31881  esumiun  32062  0elsiga  32082  ddemeas  32204  bnj168  32709  bnj593  32725  bnj607  32896  bnj600  32899  bnj916  32913  fineqvpow  33065  lfuhgr3  33081  cusgredgex  33083  loop1cycl  33099  umgr2cycl  33103  fundmpss  33740  lrrecfr  34100  exisym1  34613  bj-sylge  34805  bj-19.12  34943  bj-equs45fv  34993  bj-snsetex  35153  bj-snglss  35160  bj-snglex  35163  bj-bm1.3ii  35235  bj-restn0  35261  bj-ccinftydisj  35384  mptsnunlem  35509  pibt2  35588  wl-cbvmotv  35672  wl-moae  35675  wl-nax6im  35677  sn-iotanul  40194  iscard4  41140  ismnushort  41919  spsbce-2  41999  iotaexeu  42036  iotasbc  42037  relopabVD  42521  ax6e2ndeqVD  42529  2uasbanhVD  42531  ax6e2ndeqALT  42551  fnchoice  42572  rfcnnnub  42579  stoweidlem35  43576  stoweidlem57  43598  mo0sn  46161