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

Theorem r19.21bi 2407
 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 2311 . . . 4 (∀𝑥𝐴 𝜓 ↔ ∀𝑥(𝑥𝐴𝜓))
31, 2sylib 127 . . 3 (𝜑 → ∀𝑥(𝑥𝐴𝜓))
4319.21bi 1450 . 2 (𝜑 → (𝑥𝐴𝜓))
54imp 115 1 ((𝜑𝑥𝐴) → 𝜓)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97  ∀wal 1241   ∈ wcel 1393  ∀wral 2306 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-4 1400 This theorem depends on definitions:  df-bi 110  df-ral 2311 This theorem is referenced by:  rspec2  2408  rspec3  2409  r19.21be  2410  frind  4089  wepo  4096  wetrep  4097  ordelord  4118  ralxfr2d  4196  rexxfr2d  4197  funfveu  5188  f1oresrab  5329  isoselem  5459  tfrlemisucaccv  5939  prcdnql  6582  prcunqu  6583  prdisj  6590  caucvgsrlembound  6878  caucvgsrlemoffgt1  6883  monoord2  9236  caucvgrelemcau  9579  climrecvg1n  9867
 Copyright terms: Public domain W3C validator