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

Theorem r19.21bi 2461
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 2364 . . . 4 (∀𝑥𝐴 𝜓 ↔ ∀𝑥(𝑥𝐴𝜓))
31, 2sylib 120 . . 3 (𝜑 → ∀𝑥(𝑥𝐴𝜓))
4319.21bi 1495 . 2 (𝜑 → (𝑥𝐴𝜓))
54imp 122 1 ((𝜑𝑥𝐴) → 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wal 1287  wcel 1438  wral 2359
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-4 1445
This theorem depends on definitions:  df-bi 115  df-ral 2364
This theorem is referenced by:  rspec2  2462  rspec3  2463  r19.21be  2464  frind  4179  wepo  4186  wetrep  4187  ordelord  4208  ralxfr2d  4286  rexxfr2d  4287  funfveu  5318  f1oresrab  5463  isoselem  5599  disjxp1  6001  tfrlemisucaccv  6090  tfr1onlemsucaccv  6106  tfrcllemsucaccv  6119  xpf1o  6560  fimax2gtrilemstep  6616  supisoti  6705  exmidomni  6798  prcdnql  7043  prcunqu  7044  prdisj  7051  caucvgsrlembound  7339  caucvgsrlemoffgt1  7344  exbtwnzlemex  9661  monoord2  9905  iseqf1olemqk  9923  seq3f1olemqsumk  9928  caucvgrelemcau  10413  fimaxre2  10658  climrecvg1n  10737  zisum  10774  fisum  10778  isumss2  10785  fisumser  10790  sumpr  10807  sumtp  10808  fsum2dlemstep  10828  fsumiun  10871  isumlessdc  10890  bezoutlemstep  11264
  Copyright terms: Public domain W3C validator