ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  19.21bi Unicode version

Theorem 19.21bi 1491
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 1441 . 2  |-  ( A. x ps  ->  ps )
31, 2syl 14 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1283
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-4 1441
This theorem is referenced by:  19.21bbi  1492  ax11e  1718  eqeq1  2088  eleq2  2143  r19.21bi  2450  elrab3t  2749  ssel  2994  copsex2t  4008  pocl  4066  ordsucim  4252  peano2  4344  funmo  4947  funun  4974  fununi  4998  imain  5012  tfrlem3-2d  5961  tfr1onlemaccex  5997  tfri1dALT  6000  tfrcllemaccex  6010  findcard  6422  findcard2  6423  findcard2s  6424
  Copyright terms: Public domain W3C validator