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

Theorem 19.21v 1750
 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 (φ → ∀xφ) in 19.21 1472 via the use of distinct variable conditions combined with ax-17 1416. 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 1902 derived from df-eu 1900. 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 (x(φψ) ↔ (φxψ))
Distinct variable group:   φ,x
Allowed substitution hint:   ψ(x)

Proof of Theorem 19.21v
StepHypRef Expression
1 ax-17 1416 . 2 (φxφ)
2119.21h 1446 1 (x(φψ) ↔ (φxψ))
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 98  ∀wal 1240 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-gen 1335  ax-4 1397  ax-17 1416  ax-ial 1424  ax-i5r 1425 This theorem depends on definitions:  df-bi 110 This theorem is referenced by:  pm11.53  1772  cbval2  1793  sbhb  1813  2sb6  1857  sbcom2v  1858  2sb6rf  1863  2exsb  1882  moanim  1971  r3al  2360  ceqsralt  2575  euind  2722  reu2  2723  reuind  2738  unissb  3601  dfiin2g  3681  tfi  4248  asymref  4653  dff13  5350  mpt22eqb  5552
 Copyright terms: Public domain W3C validator