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

Theorem 19.21v 1884
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 1594 via the use of distinct variable conditions combined with ax-17 1537. 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 2047 derived from df-eu 2045. 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 1537 . 2 (𝜑 → ∀𝑥𝜑)
2119.21h 1568 1 (∀𝑥(𝜑𝜓) ↔ (𝜑 → ∀𝑥𝜓))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 105  wal 1362
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 107  ax-ia3 108  ax-5 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ial 1545  ax-i5r 1546
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  pm11.53  1907  cbval2  1933  cbvaldvaw  1942  sbhb  1956  2sb6  2000  sbcom2v  2001  2sb6rf  2006  2exsb  2025  moanim  2116  r3al  2538  ceqsralt  2787  rspc2gv  2876  euind  2947  reu2  2948  reuind  2965  unissb  3865  dfiin2g  3945  tfi  4610  asymref  5043  dff13  5803  mpo2eqb  6020
  Copyright terms: Public domain W3C validator