Theorem eximi 1868

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 1867	. 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))
2		eximi.1	. 2 ⊢ (𝜑 → 𝜓)
3	1, 2	mpg 1830	1 ⊢ (∃𝑥𝜑 → ∃𝑥𝜓)

This proof depends on syntax axioms:   → wi 4  ∃wex 1812

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-ex 1813

This theorem is used by:  2eximi  1869  eximii  1870  exa1  1871  exsimpl  1901  exsimpr  1902  19.29r2  1908  19.29x  1909  19.35  1910  19.40-2  1920  emptyex  1940  exlimiv  1963  speimfwALT  1997  nfexhe  2213  19.12  2359  ax13lem2  2407  exdistrf  2478  equs45f  2490  dfmoeu  2562  eu6  2601  2eu2ex  2670  reximi2  3097  cgsexg  3497  gencbvex  3509  eqvincg  3605  sbcg  3814  n0rex  4308  axrep2  5239  sepex  5261  bm1.3iiOLD  5263  ax6vsep  5264  axprg  5406  copsexgwOLD  5471  copsexg  5472  relopabi  5807  dmcoss  5963  dminss  6148  imainss  6149  iotanul2  6510  fv3  6900  ssimaex  6967  dffv2  6977  exfo  7102  oprabidw  7448  oprabid  7449  zfrep6OLD  7956  frxp  8128  suppimacnvss  8175  tz7.48-1  8436  enssdom  8986  enssdomOLD  8987  enfii  9184  fineqvlem  9240  enp1i  9253  infcntss  9296  infeq5  9620  rankuni  9849  scott0b  9880  scott0OLD  9881  acni3  10054  acnnum  10059  dfac3  10128  dfac9  10143  kmlem1  10157  cflm  10255  cfcof  10280  axdc4lem  10461  axcclem  10463  ac6c4  10487  ac6s  10490  ac6s2  10492  axdclem2  10526  brdom3  10535  brdom5  10536  brdom4  10537  nqpr  11027  ltexprlem4  11052  reclem2pr  11061  hash1to3  14561  trclublem  15072  fnpr2ob  17650  drsdirfi  18399  toprntopon  23156  2ndcsb  23680  fbssint  24070  isfil2  24088  alexsubALTlem3  24281  lpbl  24735  metustfbas  24789  lrrecfr  28216  lfuhgr3  29615  loop1cycl  30631  umgr2cycl  30634  ex-natded9.26-2  30908  19.9d2rf  32953  rexunirn  32975  f1ocnt  33279  fsumiunle  33307  fmcncfil  34449  esumiun  34612  0elsiga  34632  ddemeas  34755  bnj168  35248  bnj593  35263  bnj607  35433  bnj600  35436  bnj916  35450  axprALT2  35625  fineqvpow  35649  tz9.1regs  35668  kardeq0  35690  onvf1odlem1  35708  wevgblacfn  35716  cusgredgex  35728  fundmpss  36354  exisym1  37051  axtco2g  37104  bj-sylge  37345  bj-exextruan  37376  bj-cbvew  37380  bj-19.12  37464  bj-equs45fv  37562  bj-snsetex  37715  bj-snglss  37722  bj-snglex  37725  bj-bm1.3ii  37816  bj-axnul  37825  bj-axseprep  37827  bj-restn0  37848  bj-ccinftydisj  37973  mptsnunlem  38100  pibt2  38179  wl-cbvmotv  38284  wl-moae  38287  wl-nax6im  38289  eu6w  43530  iscard4  44381  ismnushort  45133  spsbce-2  45213  iotaexeu  45250  iotasbc  45251  relopabVD  45731  ax6e2ndeqVD  45739  2uasbanhVD  45741  ax6e2ndeqALT  45761  fnchoice  45871  rfcnnnub  45878  stoweidlem35  46871  stoweidlem57  46893  mo0sn  49752