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

Theorem 19.21v 1802
 Description: Special case of Theorem 19.21 of [Margaris] p. 90. Notational convention: We sometimes suffix with "v" the label of a theorem eliminating a hypothesis such as (𝜑 → ∀𝑥𝜑) in 19.21 1521 via the use of distinct variable conditions combined with ax-17 1465. Conversely, we sometimes suffix with "f" the label of a theorem introducing such a hypothesis to eliminate the need for the distinct variable condition; e.g., euf 1954 derived from df-eu 1952. The "f" stands for "not free in" which is less restrictive than "does not occur in". (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
19.21v (∀𝑥(𝜑𝜓) ↔ (𝜑 → ∀𝑥𝜓))
Distinct variable group:   𝜑,𝑥
Allowed substitution hint:   𝜓(𝑥)

Proof of Theorem 19.21v
StepHypRef Expression
1 ax-17 1465 . 2 (𝜑 → ∀𝑥𝜑)
2119.21h 1495 1 (∀𝑥(𝜑𝜓) ↔ (𝜑 → ∀𝑥𝜓))
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 104  ∀wal 1288 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 106  ax-ia3 107  ax-5 1382  ax-gen 1384  ax-4 1446  ax-17 1465  ax-ial 1473  ax-i5r 1474 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  pm11.53  1824  cbval2  1845  sbhb  1865  2sb6  1909  sbcom2v  1910  2sb6rf  1915  2exsb  1934  moanim  2023  r3al  2421  ceqsralt  2649  rspc2gv  2736  euind  2805  reu2  2806  reuind  2823  unissb  3691  dfiin2g  3771  tfi  4412  asymref  4832  dff13  5563  mpt22eqb  5770
 Copyright terms: Public domain W3C validator