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

Theorem r19.21v 2554
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 1528 . 2 𝑥𝜑
21r19.21 2553 1 (∀𝑥𝐴 (𝜑𝜓) ↔ (𝜑 → ∀𝑥𝐴 𝜓))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 105  wral 2455
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ial 1534  ax-i5r 1535
This theorem depends on definitions:  df-bi 117  df-nf 1461  df-ral 2460
This theorem is referenced by:  r19.32vdc  2626  rmo4  2932  rmo3  3056  dftr5  4106  reusv3  4462  tfrlem1  6311  tfrlemi1  6335  tfr1onlemaccex  6351  tfrcllemaccex  6364  tfri3  6370  ordiso2  7036  raluz2  9581  ndvdssub  11937  nninfalllem1  14796  nninfsellemqall  14803
  Copyright terms: Public domain W3C validator