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

Theorem r19.21bi 2424
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 2328 . . . 4 (∀𝑥𝐴 𝜓 ↔ ∀𝑥(𝑥𝐴𝜓))
31, 2sylib 131 . . 3 (𝜑 → ∀𝑥(𝑥𝐴𝜓))
4319.21bi 1466 . 2 (𝜑 → (𝑥𝐴𝜓))
54imp 119 1 ((𝜑𝑥𝐴) → 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101  wal 1257  wcel 1409  wral 2323
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-4 1416
This theorem depends on definitions:  df-bi 114  df-ral 2328
This theorem is referenced by:  rspec2  2425  rspec3  2426  r19.21be  2427  frind  4117  wepo  4124  wetrep  4125  ordelord  4146  ralxfr2d  4224  rexxfr2d  4225  funfveu  5216  f1oresrab  5357  isoselem  5487  tfrlemisucaccv  5970  supisoti  6414  prcdnql  6640  prcunqu  6641  prdisj  6648  caucvgsrlembound  6936  caucvgsrlemoffgt1  6941  monoord2  9400  caucvgrelemcau  9807  climrecvg1n  10098
  Copyright terms: Public domain W3C validator