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

Theorem r19.21bi 2424
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 20-Nov-1994.)
Hypothesis
Ref Expression
r19.21bi.1  |-  ( ph  ->  A. x  e.  A  ps )
Assertion
Ref Expression
r19.21bi  |-  ( (
ph  /\  x  e.  A )  ->  ps )

Proof of Theorem r19.21bi
StepHypRef Expression
1 r19.21bi.1 . . . 4  |-  ( ph  ->  A. x  e.  A  ps )
2 df-ral 2328 . . . 4  |-  ( A. x  e.  A  ps  <->  A. x ( x  e.  A  ->  ps )
)
31, 2sylib 131 . . 3  |-  ( ph  ->  A. x ( x  e.  A  ->  ps ) )
4319.21bi 1466 . 2  |-  ( ph  ->  ( x  e.  A  ->  ps ) )
54imp 119 1  |-  ( (
ph  /\  x  e.  A )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101   A.wal 1257    e. wcel 1409   A.wral 2323
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-4 1416
This theorem depends on definitions:  df-bi 114  df-ral 2328
This theorem is referenced by:  rspec2  2425  rspec3  2426  r19.21be  2427  frind  4117  wepo  4124  wetrep  4125  ordelord  4146  ralxfr2d  4224  rexxfr2d  4225  funfveu  5216  f1oresrab  5357  isoselem  5487  tfrlemisucaccv  5970  supisoti  6414  prcdnql  6640  prcunqu  6641  prdisj  6648  caucvgsrlembound  6936  caucvgsrlemoffgt1  6941  monoord2  9400  caucvgrelemcau  9807  climrecvg1n  10098
  Copyright terms: Public domain W3C validator