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

Theorem r19.21bi 2495
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 2396 . . . 4 (∀𝑥𝐴 𝜓 ↔ ∀𝑥(𝑥𝐴𝜓))
31, 2sylib 121 . . 3 (𝜑 → ∀𝑥(𝑥𝐴𝜓))
4319.21bi 1520 . 2 (𝜑 → (𝑥𝐴𝜓))
54imp 123 1 ((𝜑𝑥𝐴) → 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wal 1312  wcel 1463  wral 2391
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-4 1470
This theorem depends on definitions:  df-bi 116  df-ral 2396
This theorem is referenced by:  rspec2  2496  rspec3  2497  r19.21be  2498  frind  4242  wepo  4249  wetrep  4250  ordelord  4271  ralxfr2d  4353  rexxfr2d  4354  funfveu  5400  fvmptelrn  5539  f1oresrab  5551  isoselem  5687  disjxp1  6099  tfrlemisucaccv  6188  tfr1onlemsucaccv  6204  tfrcllemsucaccv  6217  xpf1o  6704  fimax2gtrilemstep  6760  supisoti  6863  difinfsn  6951  exmidomni  6980  prcdnql  7256  prcunqu  7257  prdisj  7264  caucvgsrlembound  7566  caucvgsrlemoffgt1  7571  exbtwnzlemex  9978  monoord2  10201  iseqf1olemqk  10218  seq3f1olemqsumk  10223  caucvgrelemcau  10703  fimaxre2  10949  climrecvg1n  11068  zsumdc  11104  fsum3  11107  isumss2  11113  fsum3ser  11117  sumpr  11133  sumtp  11134  fsum2dlemstep  11154  fsumiun  11197  isumlessdc  11216  bezoutlemstep  11592  ennnfonelemim  11843  cnmpt11  12358  psmet0  12402  psmettri2  12403  mulcncflem  12665  mulcncf  12666  dedekindeulemuub  12670  dedekindeulemlu  12674  dedekindicclemuub  12679  dedekindicclemlu  12683  limccnpcntop  12719  limccnp2lem  12720  limccnp2cntop  12721  nninffeq  13050  refeq  13057
  Copyright terms: Public domain W3C validator