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

Theorem 19.21bi 1766
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 1755 . 2  |-  ( A. x ps  ->  ps )
31, 2syl 16 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1546
This theorem is referenced by:  19.21bbi  1877  eqeq1  2393  eleq2  2448  r19.21bi  2747  ssel  3285  copsex2t  4384  pocl  4451  funmo  5410  funun  5435  fununi  5457  findcard  7283  findcard2  7284  axpowndlem2  8406  axpowndlem4  8408  axregndlem2  8411  axinfnd  8414  prcdnq  8803  relexpindlem  24918  dfrtrcl2  24927  vk15.4j  27955  hbimpg  27984  bnj1379  28540  bnj1052  28682  bnj1118  28691  bnj1154  28706  bnj1280  28727
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-11 1753
This theorem depends on definitions:  df-bi 178  df-ex 1548
  Copyright terms: Public domain W3C validator