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

Theorem 19.21v 1769
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 1491 via the use of distinct variable conditions combined with ax-17 1435. 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 1921 derived from df-eu 1919. 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 1435 . 2 (𝜑 → ∀𝑥𝜑)
2119.21h 1465 1 (∀𝑥(𝜑𝜓) ↔ (𝜑 → ∀𝑥𝜓))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 102  wal 1257
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-4 1416  ax-17 1435  ax-ial 1443  ax-i5r 1444
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  pm11.53  1791  cbval2  1812  sbhb  1832  2sb6  1876  sbcom2v  1877  2sb6rf  1882  2exsb  1901  moanim  1990  r3al  2383  ceqsralt  2598  rspc2gv  2684  euind  2751  reu2  2752  reuind  2767  unissb  3638  dfiin2g  3718  tfi  4333  asymref  4738  dff13  5435  mpt22eqb  5638
  Copyright terms: Public domain W3C validator