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

Theorem r19.21v 2547
Description: Theorem 19.21 of [Margaris] p. 90 with restricted quantifiers. (Contributed by NM, 15-Oct-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.)
Assertion
Ref Expression
r19.21v (∀𝑥𝐴 (𝜑𝜓) ↔ (𝜑 → ∀𝑥𝐴 𝜓))
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝐴(𝑥)

Proof of Theorem r19.21v
StepHypRef Expression
1 nfv 1521 . 2 𝑥𝜑
21r19.21 2546 1 (∀𝑥𝐴 (𝜑𝜓) ↔ (𝜑 → ∀𝑥𝐴 𝜓))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104  wral 2448
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-4 1503  ax-17 1519  ax-ial 1527  ax-i5r 1528
This theorem depends on definitions:  df-bi 116  df-nf 1454  df-ral 2453
This theorem is referenced by:  r19.32vdc  2619  rmo4  2923  rmo3  3046  dftr5  4088  reusv3  4443  tfrlem1  6284  tfrlemi1  6308  tfr1onlemaccex  6324  tfrcllemaccex  6337  tfri3  6343  ordiso2  7008  raluz2  9525  ndvdssub  11876  nninfalllem1  13963  nninfsellemqall  13970
  Copyright terms: Public domain W3C validator