Theorem 19.22i 1076

Description: Inference adding existential quantifier to antecedent and consequent.

Hypothesis

Ref	Expression
19.22i.1	|- (ph -> ps)

Assertion

Ref	Expression
19.22i	|- (E.xph -> E.xps)

Proof of Theorem 19.22i

Step	Hyp	Ref	Expression
1		19.22 1075	. 2 |- (A.x(ph -> ps) -> (E.xph -> E.xps))
2		19.22i.1	. 2 |- (ph -> ps)
3	1, 2	mpg 1022	1 |- (E.xph -> E.xps)

Syntax hints:   -> wi 3  E.wex 1016

This theorem is referenced by:  19.22i2 1077  19.12 1083  19.23ai 1100  19.29r2 1109  19.29x 1110  19.40 1130  equvini 1205  sbimi 1210  equs45f 1237  sbequi 1265  mo 1432  eumo0 1434  eupickb 1475  mopick2 1476  euor2 1477  moexex 1478  2euex 1481  2eu2ex 1483  2exeu 1486  rexex 1739  r19.22i2 1779  cgsexg 1877  vtoclf 1887  vtocl3 1890  cla4gf 1906  ssiun 2660  iununi 2686  axrep1 2768  axrep2 2769  axsep 2776  bm1.3ii 2780  axnul 2783  nalset 2786  notzfaus 2815  el 2822  dtru 2831  dvdemo1 2851  dvdemo2 2852  axpr 2854  snnex 3100  euuni 3105  dmcoss 3450  dmcosseq 3452  imassrn 3507  dminss 3547  imainss 3548  zfrep6 3721  fv3 3844  ssimaex 3879  exfo 3936  abrexexlem1 3972  tz7.48-1 4257  uniixp 4498  enssdom 4524  unblem2 4687  infcntss 4699  abfii2 4705  abfii4 4707  fodomfi 4709  inf1 4752  infeq5 4766  omex 4772  rankuni 4844  scott0 4863  bnd 4869  aceq3 4879  aceq4 4880  ac5b 4899  ac6 4901  ac6s 4902  ac6s2 4904  ac6s3 4905  ac6s5 4908  kmlem1 4911  kmlem2 4912  kmlem8 4918  brdom3 4947  brdom5 4948  brdom4 4949  cflim 5059  axpowndlem2 5104  axacndlem4 5116  prnmadd 5254  1idpr 5287  ltexprlem4 5299  reclem1pr 5310  reclem2pr 5311  recexpr 5314  suplem1pr 5315  suplem2pr 5316  recexsrlem 5366  suppsr2 5377  suppsr3 5378  pre-axsup 5445  0re 5594  infcvglem3 7427  infxpidmlem8 7771  infmap2lem1 7791  subbas 7856  subtop 7858  grothinf 9053  osumlem5 9860  eqindhome 11047  rcfpfillem3 11091  r19.2zb 11393  alexsublem3 11498  fnejoin2 11592  fgfil 11638  oprabopabf 11807  heiborlem13 12023  heiborlem17 12027  heiborlem37 12047

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 999  ax-4 1009  ax-5o 1011

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1017

Copyright terms: Public domain