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

Theorem r19.21bi 2462
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 2365 . . . 4 (∀𝑥𝐴 𝜓 ↔ ∀𝑥(𝑥𝐴𝜓))
31, 2sylib 121 . . 3 (𝜑 → ∀𝑥(𝑥𝐴𝜓))
4319.21bi 1496 . 2 (𝜑 → (𝑥𝐴𝜓))
54imp 123 1 ((𝜑𝑥𝐴) → 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wal 1288  wcel 1439  wral 2360
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-4 1446
This theorem depends on definitions:  df-bi 116  df-ral 2365
This theorem is referenced by:  rspec2  2463  rspec3  2464  r19.21be  2465  frind  4188  wepo  4195  wetrep  4196  ordelord  4217  ralxfr2d  4299  rexxfr2d  4300  funfveu  5331  f1oresrab  5477  isoselem  5613  disjxp1  6015  tfrlemisucaccv  6104  tfr1onlemsucaccv  6120  tfrcllemsucaccv  6133  xpf1o  6614  fimax2gtrilemstep  6670  supisoti  6759  exmidomni  6859  prcdnql  7104  prcunqu  7105  prdisj  7112  caucvgsrlembound  7400  caucvgsrlemoffgt1  7405  exbtwnzlemex  9722  monoord2  9966  iseqf1olemqk  9984  seq3f1olemqsumk  9989  caucvgrelemcau  10474  fimaxre2  10719  climrecvg1n  10798  zisum  10835  fisum  10839  isumss2  10846  fisumser  10851  sumpr  10868  sumtp  10869  fsum2dlemstep  10889  fsumiun  10932  isumlessdc  10951  bezoutlemstep  11325
  Copyright terms: Public domain W3C validator