Theorem eximi 1387

Description: Inference adding existential quantifier to antecedent and consequent.

Hypothesis

Ref	Expression
eximi.1	|- (ph -> ps)

Assertion

Ref	Expression
eximi	|- (E.xph -> E.xps)

Proof of Theorem eximi

Step	Hyp	Ref	Expression
1		exim 1386	. 2 |- (A.x(ph -> ps) -> (E.xph -> E.xps))
2		eximi.1	. 2 |- (ph -> ps)
3	1, 2	mpg 1332	1 |- (E.xph -> E.xps)

Syntax hints:   -> wi 3  E.wex 1326

This theorem is referenced by:  2eximi 1388  19.12 1394  19.23aiOLD 1413  19.29r2 1424  19.29x 1425  19.40 1447  exsimpl 1461  equvini 1531  equviniOLD 1532  sbimi 1537  equs45f 1569  sbequi 1598  mo 1787  eumo0 1790  euan 1827  eupickb 1836  euor2OLD 1840  2euexOLD 1845  2eu2ex 1847  2exeu 1850  rexex 2154  reximi2 2197  cgsexg 2321  gencbvex 2334  vtoclf 2338  vtocl3 2342  vtocl3OLD 2343  cla4gf 2361  cla4gfOLD 2363  eqvinc 2387  ssiunOLD 3294  iununi 3331  iununiOLD 3332  axrep1 3429  axrep2 3430  axsep 3437  bm1.3ii 3441  axnul 3444  nalset 3448  notzfaus 3478  el 3485  elOLD 3486  dtru 3498  dvdemo1 3520  dvdemo2 3521  axpr 3523  snnex 3801  euuni 3807  eufromeq3 3830  dmcossOLD 4212  imassrn 4278  dminss 4330  imainss 4331  dmsnop 4367  zfrep6 4545  fv3 4690  ssimaex 4729  dffv2 4734  exfo 4795  abrexexlem1 4834  iotaex 5099  tz7.48-1 5165  uniixp 5416  enssdom 5442  infcntss 5646  abfii2 5652  abfii4 5654  fodomfi 5656  inf1 5713  infeq5 5727  omex 5733  rankuni 5809  scott0 5847  bnd 5853  aceq3 5895  aceq4 5896  ac5b 5915  ac6 5917  ac6s 5918  ac6s2 5920  ac6s3 5921  ac6s5 5924  kmlem1 5927  kmlem2 5928  brdom3 5963  brdom5 5964  brdom4 5965  cflim 6057  axpowndlem2 6102  axacndlem4 6114  prnmadd 6252  1idpr 6285  ltexprlem4 6297  reclem1pr 6308  reclem2pr 6309  recexpr 6312  suplem1pr 6313  suplem2pr 6314  recexsrlem 6364  suppsr2 6375  suppsr3 6376  pre-axsup 6444  infcvglem3 8484  infxpidmlem8 8828  infmap2lem1 8848  subbas 8914  subtop 8916  grothomex 10136  oprabopabf 10157  fgfil 10290  osumlem5 11217  bnj90OLD 12446  bnj101 12448  bnj161 12486  bnj168 12496  bnj214 12508  bnj512 12519  bnj542 12536  bnj577 12549  bnj593 12556  bnj880 12807  bnj123 13233  bnj514 13255  bnj605 13292  bnj607 13304  bnj849 13318  bnj894 13327  bnj916 13332  bnj936 13336  bnj1125 13430  bnj1498 13562  fundmpss 13836  axextdfeq 13864  ax13dfeq 13865  axextndbi 13871  frxp 13951  exisym1 14248  dstr 14516  eqindhome 14895  rcfpfillem3 14930  alexsublem3 15439  fnejoin2 15531  heiborlem13 15967  heiborlem17 15971  heiborlem37 15991  exan3 16241  prtlem16 16272  a4sbce-2 16333  19.40-2 16334  iotaexeu 16382  iotasbc 16383

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-4 1319  ax-5o 1321

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327

Copyright terms: Public domain