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

Theorem 19.21v 1753
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 1475 via the use of distinct variable conditions combined with ax-17 1419. 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 1905 derived from df-eu 1903. 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 1419 . 2 (𝜑 → ∀𝑥𝜑)
2119.21h 1449 1 (∀𝑥(𝜑𝜓) ↔ (𝜑 → ∀𝑥𝜓))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98  wal 1241
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-4 1400  ax-17 1419  ax-ial 1427  ax-i5r 1428
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  pm11.53  1775  cbval2  1796  sbhb  1816  2sb6  1860  sbcom2v  1861  2sb6rf  1866  2exsb  1885  moanim  1974  r3al  2366  ceqsralt  2581  euind  2728  reu2  2729  reuind  2744  unissb  3610  dfiin2g  3690  tfi  4305  asymref  4710  dff13  5407  mpt22eqb  5610
  Copyright terms: Public domain W3C validator