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

Theorem 19.21v 1829
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 1547 via the use of distinct variable conditions combined with ax-17 1491. 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 1982 derived from df-eu 1980. 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 1491 . 2  |-  ( ph  ->  A. x ph )
2119.21h 1521 1  |-  ( A. x ( ph  ->  ps )  <->  ( ph  ->  A. x ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104   A.wal 1314
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 106  ax-ia3 107  ax-5 1408  ax-gen 1410  ax-4 1472  ax-17 1491  ax-ial 1499  ax-i5r 1500
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  pm11.53  1851  cbval2  1873  sbhb  1893  2sb6  1937  sbcom2v  1938  2sb6rf  1943  2exsb  1962  moanim  2051  r3al  2454  ceqsralt  2687  rspc2gv  2775  euind  2844  reu2  2845  reuind  2862  unissb  3736  dfiin2g  3816  tfi  4466  asymref  4894  dff13  5637  mpo2eqb  5848
  Copyright terms: Public domain W3C validator