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

Theorem 19.21v 1827
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  ( ph  ->  A. x ph ) in 19.21 1545 via the use of distinct variable conditions combined with ax-17 1489. 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 1980 derived from df-eu 1978. 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  |-  ( A. x ( ph  ->  ps )  <->  ( ph  ->  A. x ps ) )
Distinct variable group:    ph, x
Allowed substitution hint:    ps( x)

Proof of Theorem 19.21v
StepHypRef Expression
1 ax-17 1489 . 2  |-  ( ph  ->  A. x ph )
2119.21h 1519 1  |-  ( A. x ( ph  ->  ps )  <->  ( ph  ->  A. x ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104   A.wal 1312
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-gen 1408  ax-4 1470  ax-17 1489  ax-ial 1497  ax-i5r 1498
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  pm11.53  1849  cbval2  1871  sbhb  1891  2sb6  1935  sbcom2v  1936  2sb6rf  1941  2exsb  1960  moanim  2049  r3al  2452  ceqsralt  2685  rspc2gv  2773  euind  2842  reu2  2843  reuind  2860  unissb  3734  dfiin2g  3814  tfi  4464  asymref  4892  dff13  5635  mpo2eqb  5846
  Copyright terms: Public domain W3C validator