Theorem 19.22i 1081

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

Syntax hints:   -> wi 3  E.wex 1021

This theorem is referenced by:  19.22i2 1082  19.12 1088  19.23ai 1105  19.29r2 1114  19.29x 1115  19.40 1135  equvini 1210  sbimi 1215  equs45f 1242  sbequi 1270  mo 1435  eumo0 1437  eupickb 1478  mopick2 1479  euor2 1480  moexex 1481  2euex 1484  2eu2ex 1486  2exeu 1489  euequ1OLD 1501  rexex 1740  r19.22i2 1780  cgsexg 1878  vtoclf 1888  vtocl3 1891  cla4gf 1907  ssiun 2646  iununi 2671  axrep1 2749  axrep2 2750  axsep 2757  bm1.3ii 2761  axnul 2764  nalset 2767  notzfaus 2796  dtruALT 2804  dvdemo1 2831  dvdemo2 2832  axpr 2834  snnex 2933  euuni 2938  dmcoss 3420  dmcosseq 3422  imassrn 3472  dminss 3519  imainss 3520  zfrep6 3671  fv3 3790  ssimaex 3825  exfo 3879  abrexexlem1 3915  tz7.48-1 4014  uniixp 4418  enssdom 4444  unblem2 4604  infcntss 4616  abfii2 4622  abfii4 4624  fodomfi 4626  inf1 4669  infeq5 4683  omex 4689  rankuni 4760  scott0 4779  bnd 4785  aceq3 4795  aceq4 4796  ac5b 4815  ac6 4817  ac6s 4818  ac6s2 4820  ac6s3 4821  ac6s5 4824  kmlem1 4827  kmlem2 4828  kmlem8 4834  brdom3 4863  brdom5 4864  brdom4 4865  cflim 4974  axpowndlem2 5015  axacndlem4 5027  prnmadd 5165  1idpr 5198  ltexprlem4 5210  reclem1pr 5221  reclem2pr 5222  recexpr 5225  suplem1pr 5226  suplem2pr 5227  recexsrlem 5277  suppsr2 5288  suppsr3 5289  pre-axsup 5356  0re 5505  infcvglem3 7313  infxpidmlem8 7651  infmap2lem1 7671  subtop 7733  grothinf 8864  osumlem5 9665  eqindhome 10635  rcfpfillem3 10673

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1004  ax-4 1014  ax-5o 1016

This theorem depends on definitions:  df-bi 154  df-an 232  df-ex 1022

Copyright terms: Public domain