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

Theorem r19.21bi 2552
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 2447 . . . 4  |-  ( A. x  e.  A  ps  <->  A. x ( x  e.  A  ->  ps )
)
31, 2sylib 121 . . 3  |-  ( ph  ->  A. x ( x  e.  A  ->  ps ) )
4319.21bi 1545 . 2  |-  ( ph  ->  ( x  e.  A  ->  ps ) )
54imp 123 1  |-  ( (
ph  /\  x  e.  A )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103   A.wal 1340    e. wcel 2135   A.wral 2442
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-4 1497
This theorem depends on definitions:  df-bi 116  df-ral 2447
This theorem is referenced by:  rspec2  2553  rspec3  2554  r19.21be  2555  frind  4325  wepo  4332  wetrep  4333  ordelord  4354  ralxfr2d  4437  rexxfr2d  4438  funfveu  5494  fvmptelrn  5633  f1oresrab  5645  isoselem  5783  disjxp1  6196  tfrlemisucaccv  6285  tfr1onlemsucaccv  6301  tfrcllemsucaccv  6314  xpf1o  6802  fimax2gtrilemstep  6858  supisoti  6967  difinfsn  7057  exmidomni  7098  cc3  7201  prcdnql  7417  prcunqu  7418  prdisj  7425  caucvgsrlembound  7727  caucvgsrlemoffgt1  7732  exbtwnzlemex  10176  monoord2  10403  iseqf1olemqk  10420  seq3f1olemqsumk  10425  caucvgrelemcau  10909  fimaxre2  11155  climrecvg1n  11276  zsumdc  11312  fsum3  11315  isumss2  11321  fsum3ser  11325  sumpr  11341  sumtp  11342  fsum2dlemstep  11362  fsumiun  11405  isumlessdc  11424  zproddc  11507  fprodsplitdc  11524  fprodcl2lem  11533  fprod2dlemstep  11550  bezoutlemstep  11916  ennnfonelemim  12311  ctiunctal  12328  cnmpt11  12841  psmet0  12885  psmettri2  12886  mulcncflem  13148  mulcncf  13149  dedekindeulemuub  13153  dedekindeulemlu  13157  dedekindicclemuub  13162  dedekindicclemlu  13166  limccnpcntop  13202  limccnp2lem  13203  limccnp2cntop  13204  bj-charfundc  13542  bj-charfunbi  13545  nninffeq  13752  refeq  13759  iswomni0  13782  nconstwlpolem  13795
  Copyright terms: Public domain W3C validator