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

Theorem 19.21bi 1520
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 1470 . 2  |-  ( A. x ps  ->  ps )
31, 2syl 14 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1312
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-4 1470
This theorem is referenced by:  19.21bbi  1521  ax11e  1750  eqeq1  2122  eleq2  2179  r19.21bi  2495  elrab3t  2810  ssel  3059  exmidsssn  4093  copsex2t  4135  pocl  4193  ordsucim  4384  peano2  4477  funmo  5106  funun  5135  fununi  5159  imain  5173  tfrlem3-2d  6175  tfr1onlemaccex  6211  tfri1dALT  6214  tfrcllemaccex  6224  findcard  6748  findcard2  6749  findcard2s  6750  exmidpw  6768
  Copyright terms: Public domain W3C validator