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

Theorem r19.21bi 2520
 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
Assertion
Ref Expression
r19.21bi

Proof of Theorem r19.21bi
StepHypRef Expression
1 r19.21bi.1 . . . 4
2 df-ral 2421 . . . 4
31, 2sylib 121 . . 3
4319.21bi 1537 . 2
54imp 123 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 103  wal 1329   wcel 1480  wral 2416 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-4 1487 This theorem depends on definitions:  df-bi 116  df-ral 2421 This theorem is referenced by:  rspec2  2521  rspec3  2522  r19.21be  2523  frind  4274  wepo  4281  wetrep  4282  ordelord  4303  ralxfr2d  4385  rexxfr2d  4386  funfveu  5434  fvmptelrn  5573  f1oresrab  5585  isoselem  5721  disjxp1  6133  tfrlemisucaccv  6222  tfr1onlemsucaccv  6238  tfrcllemsucaccv  6251  xpf1o  6738  fimax2gtrilemstep  6794  supisoti  6897  difinfsn  6985  exmidomni  7014  prcdnql  7292  prcunqu  7293  prdisj  7300  caucvgsrlembound  7602  caucvgsrlemoffgt1  7607  exbtwnzlemex  10027  monoord2  10250  iseqf1olemqk  10267  seq3f1olemqsumk  10272  caucvgrelemcau  10752  fimaxre2  10998  climrecvg1n  11117  zsumdc  11153  fsum3  11156  isumss2  11162  fsum3ser  11166  sumpr  11182  sumtp  11183  fsum2dlemstep  11203  fsumiun  11246  isumlessdc  11265  bezoutlemstep  11685  ennnfonelemim  11937  cnmpt11  12452  psmet0  12496  psmettri2  12497  mulcncflem  12759  mulcncf  12760  dedekindeulemuub  12764  dedekindeulemlu  12768  dedekindicclemuub  12773  dedekindicclemlu  12777  limccnpcntop  12813  limccnp2lem  12814  limccnp2cntop  12815  nninffeq  13216  refeq  13223
 Copyright terms: Public domain W3C validator