Theorem r19.21bi 2585

Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 20-Nov-1994.)

Hypothesis

Ref	Expression
r19.21bi.1	|- ( ph -> A. x e. A ps )

Assertion

Ref	Expression
r19.21bi	|- ( ( ph /\ x e. A ) -> ps )

Proof of Theorem r19.21bi

Step	Hyp	Ref	Expression
1		r19.21bi.1	. . . 4 |- ( ph -> A. x e. A ps )
2		df-ral 2480	. . . 4 |- ( A. x e. A ps <-> A. x ( x e. A -> ps ) )
3	1, 2	sylib 122	. . 3 |- ( ph -> A. x ( x e. A -> ps ) )
4	3	19.21bi 1572	. 2 |- ( ph -> ( x e. A -> ps ) )
5	4	imp 124	1 |- ( ( ph /\ x e. A ) -> ps )

Syntax hints:   -> wi 4   /\ wa 104   A.wal 1362   e. wcel 2167   A.wral 2475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-4 1524

This theorem depends on definitions:  df-bi 117  df-ral 2480

This theorem is referenced by:  rspec2  2586  rspec3  2587  r19.21be  2588  frind  4387  wepo  4394  wetrep  4395  ordelord  4416  ralxfr2d  4499  rexxfr2d  4500  funfveu  5571  fvmptelcdm  5715  f1oresrab  5727  isoselem  5867  mpoexw  6271  disjxp1  6294  tfrlemisucaccv  6383  tfr1onlemsucaccv  6399  tfrcllemsucaccv  6412  xpf1o  6905  fimax2gtrilemstep  6961  supisoti  7076  difinfsn  7166  exmidomni  7208  cc3  7335  prcdnql  7551  prcunqu  7552  prdisj  7559  caucvgsrlembound  7861  caucvgsrlemoffgt1  7866  exbtwnzlemex  10339  monoord2  10578  iseqf1olemqk  10599  seq3f1olemqsumk  10604  caucvgrelemcau  11145  fimaxre2  11392  climrecvg1n  11513  zsumdc  11549  fsum3  11552  isumss2  11558  fsum3ser  11562  sumpr  11578  sumtp  11579  fsum2dlemstep  11599  fsumiun  11642  isumlessdc  11661  zproddc  11744  fprodsplitdc  11761  fprodcl2lem  11770  fprod2dlemstep  11787  bezoutlemstep  12164  ennnfonelemim  12641  ctiunctal  12658  grppropd  13149  srgdilem  13525  srgrz  13540  srglz  13541  cnmpt11  14519  psmet0  14563  psmettri2  14564  mulcncflem  14843  mulcncf  14844  dedekindeulemuub  14853  dedekindeulemlu  14857  dedekindicclemuub  14862  dedekindicclemlu  14866  limccnpcntop  14911  limccnp2lem  14912  limccnp2cntop  14913  plycoeid3  14993  fsumdvdsmul  15227  bj-charfundc  15454  bj-charfunbi  15457  nninffeq  15664  refeq  15672  iswomni0  15695  nconstwlpolem  15709