Theorem 19.22i 1038

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

Syntax hints:   -> wi 3  E.wex 978

This theorem is referenced by:  19.22i2 1039  19.12 1045  19.23ai 1062  19.29r2 1071  19.29x 1072  19.40 1092  equvini 1166  sbimi 1171  equs45f 1198  sbequi 1226  mo 1391  eumo0 1393  eupickb 1433  mopick2 1434  euor2 1435  moexex 1436  2euex 1439  2eu2ex 1441  2exeu 1444  rexex 1690  r19.22i2 1730  cgsexg 1827  vtoclf 1837  vtocl3 1840  cla4gf 1856  ssiun 2587  iununi 2611  axrep1 2689  axrep2 2690  axsep 2697  bm1.3ii 2701  axnul 2704  nalset 2707  notzfaus 2736  dtruALT 2743  dvdemo1 2770  dvdemo2 2771  axpr 2773  euuni 2876  dmcoss 3355  dmcosseq 3357  imassrn 3407  dminss 3454  imainss 3455  zfrep6 3606  fv3 3724  ssimaex 3759  exfo 3813  abrexexlem1 3849  tz7.48-1 3947  uniixp 4347  enssdom 4370  unblem2 4524  infcntss 4536  abfii2 4542  abfii4 4544  fodomfi 4546  inf1 4587  infeq5 4601  omex 4607  rankuni 4678  scott0 4697  bnd 4703  aceq3 4713  aceq4 4714  ac5b 4733  ac6 4735  ac6s 4736  ac6s2 4738  ac6s3 4739  ac6s5 4742  kmlem1 4745  kmlem2 4746  kmlem8 4752  brdom3 4781  brdom5 4782  brdom4 4783  cflim 4889  axpowndlem2 4930  axacndlem4 4942  prnmadd 5080  1idpr 5113  ltexprlem4 5125  reclem1pr 5136  reclem2pr 5137  recexpr 5140  suplem1pr 5141  suplem2pr 5142  recexsrlem 5192  suppsr2 5203  suppsr3 5204  pre-axsup 5271  0re 5420  infcvglem3 7166  infxpidmlem8 7510  infmap2lem1 7529  subbas 7594  subtop 7596  grothinf 8720  osumlem5 9522

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 961  ax-4 971  ax-5o 973

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

Copyright terms: Public domain