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

Theorem r19.21bi 2565
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 2460 . . . 4 (∀𝑥𝐴 𝜓 ↔ ∀𝑥(𝑥𝐴𝜓))
31, 2sylib 122 . . 3 (𝜑 → ∀𝑥(𝑥𝐴𝜓))
4319.21bi 1558 . 2 (𝜑 → (𝑥𝐴𝜓))
54imp 124 1 ((𝜑𝑥𝐴) → 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wal 1351  wcel 2148  wral 2455
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-4 1510
This theorem depends on definitions:  df-bi 117  df-ral 2460
This theorem is referenced by:  rspec2  2566  rspec3  2567  r19.21be  2568  frind  4352  wepo  4359  wetrep  4360  ordelord  4381  ralxfr2d  4464  rexxfr2d  4465  funfveu  5528  fvmptelcdm  5669  f1oresrab  5681  isoselem  5820  mpoexw  6213  disjxp1  6236  tfrlemisucaccv  6325  tfr1onlemsucaccv  6341  tfrcllemsucaccv  6354  xpf1o  6843  fimax2gtrilemstep  6899  supisoti  7008  difinfsn  7098  exmidomni  7139  cc3  7266  prcdnql  7482  prcunqu  7483  prdisj  7490  caucvgsrlembound  7792  caucvgsrlemoffgt1  7797  exbtwnzlemex  10249  monoord2  10476  iseqf1olemqk  10493  seq3f1olemqsumk  10498  caucvgrelemcau  10988  fimaxre2  11234  climrecvg1n  11355  zsumdc  11391  fsum3  11394  isumss2  11400  fsum3ser  11404  sumpr  11420  sumtp  11421  fsum2dlemstep  11441  fsumiun  11484  isumlessdc  11503  zproddc  11586  fprodsplitdc  11603  fprodcl2lem  11612  fprod2dlemstep  11629  bezoutlemstep  11997  ennnfonelemim  12424  ctiunctal  12441  grppropd  12892  srgdilem  13150  srgrz  13165  srglz  13166  cnmpt11  13719  psmet0  13763  psmettri2  13764  mulcncflem  14026  mulcncf  14027  dedekindeulemuub  14031  dedekindeulemlu  14035  dedekindicclemuub  14040  dedekindicclemlu  14044  limccnpcntop  14080  limccnp2lem  14081  limccnp2cntop  14082  bj-charfundc  14496  bj-charfunbi  14499  nninffeq  14705  refeq  14712  iswomni0  14735  nconstwlpolem  14748
  Copyright terms: Public domain W3C validator