Theorem 19.22i 1036

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 1035	. 2 |- (A.x(ph -> ps) -> (E.xph -> E.xps))
2		19.22i.1	. 2 |- (ph -> ps)
3	1, 2	mpg 983	1 |- (E.xph -> E.xps)

Syntax hints:   -> wi 3  E.wex 977

This theorem is referenced by:  19.22i2 1037  19.12 1043  19.23ai 1060  19.29r2 1069  19.29x 1070  19.40 1090  equvini 1164  sbimi 1169  equs45f 1196  sbequi 1223  mo 1386  eumo0 1388  eupickb 1428  mopick2 1429  euor2 1430  moexex 1431  2euex 1434  2eu2ex 1436  2exeu 1439  rexex 1685  r19.22i2 1725  cgsexg 1822  vtoclf 1832  vtocl3 1835  cla4gf 1851  ssiun 2582  iununi 2606  axrep1 2684  axrep2 2685  axsep 2692  bm1.3ii 2696  axnul 2699  nalset 2702  notzfaus 2731  dtruALT 2738  dvdemo1 2765  dvdemo2 2766  axpr 2768  euuni 2871  dmcoss 3347  dmcosseq 3349  imassrn 3399  dminss 3448  imainss 3449  zfrep6 3600  fv3 3718  ssimaex 3753  exfo 3807  abrexexlem1 3843  tz7.48-1 3941  uniixp 4341  enssdom 4364  unblem2 4518  infcntss 4530  abfii2 4536  abfii4 4538  fodomfi 4540  inf1 4579  infeq5 4593  omex 4599  rankuni 4670  scott0 4689  bnd 4695  aceq3 4705  aceq4 4706  ac5b 4725  ac6 4727  ac6s 4728  ac6s2 4730  ac6s3 4731  ac6s5 4734  kmlem1 4737  kmlem2 4738  kmlem8 4744  brdom3 4773  brdom5 4774  brdom4 4775  cflim 4881  axpowndlem2 4922  axacndlem4 4934  prnmadd 5072  1idpr 5105  ltexprlem4 5117  reclem1pr 5128  reclem2pr 5129  recexpr 5132  suplem1pr 5133  suplem2pr 5134  recexsrlem 5184  suppsr2 5195  suppsr3 5196  pre-axsup 5263  0re 5412  infcvglem3 7158  infxpidmlem8 7502  infmap2lem1 7521  subbas 7586  subtop 7588  grothinf 8720  osumlem5 9499

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-4 970  ax-5o 972

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978

Copyright terms: Public domain