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

Theorem 19.21v 1801
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 1520 via the use of distinct variable conditions combined with ax-17 1464. 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 1953 derived from df-eu 1951. 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 1464 . 2 (𝜑 → ∀𝑥𝜑)
2119.21h 1494 1 (∀𝑥(𝜑𝜓) ↔ (𝜑 → ∀𝑥𝜓))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103  wal 1287
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-gen 1383  ax-4 1445  ax-17 1464  ax-ial 1472  ax-i5r 1473
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  pm11.53  1823  cbval2  1844  sbhb  1864  2sb6  1908  sbcom2v  1909  2sb6rf  1914  2exsb  1933  moanim  2022  r3al  2420  ceqsralt  2646  rspc2gv  2733  euind  2802  reu2  2803  reuind  2820  unissb  3683  dfiin2g  3763  tfi  4397  asymref  4817  dff13  5547  mpt22eqb  5754
  Copyright terms: Public domain W3C validator