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

Theorem 19.21v 1866
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 1576 via the use of distinct variable conditions combined with ax-17 1519. 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 2024 derived from df-eu 2022. 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 1519 . 2 (𝜑 → ∀𝑥𝜑)
2119.21h 1550 1 (∀𝑥(𝜑𝜓) ↔ (𝜑 → ∀𝑥𝜓))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104  wal 1346
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-4 1503  ax-17 1519  ax-ial 1527  ax-i5r 1528
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  pm11.53  1888  cbval2  1914  sbhb  1933  2sb6  1977  sbcom2v  1978  2sb6rf  1983  2exsb  2002  moanim  2093  r3al  2514  ceqsralt  2757  rspc2gv  2846  euind  2917  reu2  2918  reuind  2935  unissb  3826  dfiin2g  3906  tfi  4566  asymref  4996  dff13  5747  mpo2eqb  5962
  Copyright terms: Public domain W3C validator