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  2214  19.12  2363  ax13lem2  2411  exdistrf  2482  equs45f  2494  dfmoeu  2566  eu6  2605  2eu2ex  2674  reximi2  3101  cgsexg  3502  gencbvex  3514  eqvincg  3610  sbcg  3819  n0rex  4315  axrep2  5246  sepex  5268  bm1.3iiOLD  5270  ax6vsep  5271  axprg  5413  copsexgwOLD  5478  copsexg  5479  relopabi  5814  dmcoss  5970  dminss  6155  imainss  6156  iotanul2  6516  fv3  6906  ssimaex  6973  dffv2  6983  exfo  7107  oprabidw  7454  oprabid  7455  zfrep6OLD  7961  frxp  8131  suppimacnvss  8178  tz7.48-1  8439  enssdom  8982  enssdomOLD  8983  enfii  9180  fineqvlem  9236  enp1i  9249  infcntss  9292  infeq5  9616  rankuni  9845  scott0b  9876  scott0OLD  9877  acni3  10050  acnnum  10055  dfac3  10124  dfac9  10139  kmlem1  10153  cflm  10251  cfcof  10276  axdc4lem  10457  axcclem  10459  ac6c4  10483  ac6s  10486  ac6s2  10488  axdclem2  10522  brdom3  10530  brdom5  10531  brdom4  10532  nqpr  11017  ltexprlem4  11042  reclem2pr  11051  hash1to3  14549  trclublem  15058  fnpr2ob  17637  drsdirfi  18386  toprntopon  23119  2ndcsb  23643  fbssint  24032  isfil2  24050  alexsubALTlem3  24243  lpbl  24697  metustfbas  24751  lrrecfr  28173  ex-natded9.26-2  30808  19.9d2rf  32853  rexunirn  32875  f1ocnt  33182  fsumiunle  33210  fmcncfil  34352  esumiun  34515  0elsiga  34535  ddemeas  34658  bnj168  35151  bnj593  35166  bnj607  35336  bnj600  35339  bnj916  35353  axprALT2  35528  fineqvpow  35552  tz9.1regs  35571  kardeq0  35593  onvf1odlem1  35611  wevgblacfn  35619  lfuhgr3  35633  cusgredgex  35635  loop1cycl  35650  umgr2cycl  35654  fundmpss  36280  exisym1  36976  axtco2g  37029  bj-sylge  37270  bj-exextruan  37301  bj-cbvew  37305  bj-19.12  37389  bj-equs45fv  37487  bj-snsetex  37640  bj-snglss  37647  bj-snglex  37650  bj-bm1.3ii  37741  bj-axnul  37750  bj-axseprep  37752  bj-restn0  37773  bj-ccinftydisj  37898  mptsnunlem  38025  pibt2  38104  wl-cbvmotv  38209  wl-moae  38212  wl-nax6im  38214  eu6w  43449  iscard4  44300  ismnushort  45052  spsbce-2  45132  iotaexeu  45169  iotasbc  45170  relopabVD  45650  ax6e2ndeqVD  45658  2uasbanhVD  45660  ax6e2ndeqALT  45680  fnchoice  45790  rfcnnnub  45797  stoweidlem35  46790  stoweidlem57  46812  mo0sn  49635