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 ax-4 1692 . 2  |-  ( A. x ps  ->  ps )
31, 2syl 17 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 6   A.wal 1532
This theorem is referenced by:  19.21bbi  1775  eqeq1  2262  eleq2  2317  r19.21bi  2614  ssel  3135  copsex2t  4211  pocl  4279  funmo  5196  funun  5220  fununi  5240  findcard  7051  findcard2  7052  axpowndlem2  8174  axpowndlem4  8176  axregndlem2  8179  axinfnd  8182  prcdnq  8571  relexpindlem  23394  dfrtrcl2  23403  imfstnrelc  24433  cmpmon  25168  vk15.4j  27328  hbimpg  27357  bnj1379  27896  bnj1052  28038  bnj1118  28047  bnj1154  28062  bnj1280  28083
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-mp 10  ax-4 1692
  Copyright terms: Public domain W3C validator