MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  19.21bi Unicode version

Theorem 19.21bi 1774
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
19.21bi.1  |-  ( ph  ->  A. x ps )
Assertion
Ref Expression
19.21bi  |-  ( ph  ->  ps )

Proof of Theorem 19.21bi
StepHypRef Expression
1 19.21bi.1 . 2  |-  ( ph  ->  A. x ps )
2 sp 1763 . 2  |-  ( A. x ps  ->  ps )
31, 2syl 16 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1549
This theorem is referenced by:  19.21bbi  1888  equveli  2081  eqeq1  2441  eleq2  2496  r19.21bi  2796  ssel  3334  copsex2t  4435  pocl  4502  funmo  5461  funun  5486  fununi  5508  findcard  7338  findcard2  7339  axpowndlem2  8462  axpowndlem4  8464  axregndlem2  8467  axinfnd  8470  prcdnq  8859  relexpindlem  25127  dfrtrcl2  25136  vk15.4j  28467  hbimpg  28496  bnj1379  29056  bnj1052  29198  bnj1118  29207  bnj1154  29222  bnj1280  29243
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-ex 1551
  Copyright terms: Public domain W3C validator