Theorem 19.21v 1845

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 1562 via the use of distinct variable conditions combined with ax-17 1506. 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 2004 derived from df-eu 2002. 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

Step	Hyp	Ref	Expression
1		ax-17 1506	. 2 |- ( ph -> A. x ph )
2	1	19.21h 1536	1 |- ( A. x ( ph -> ps ) <-> ( ph -> A. x ps ) )

Syntax hints:   -> wi 4   <-> wb 104   A.wal 1329

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ial 1514  ax-i5r 1515

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm11.53  1867  cbval2  1893  sbhb  1913  2sb6  1959  sbcom2v  1960  2sb6rf  1965  2exsb  1984  moanim  2073  r3al  2477  ceqsralt  2713  rspc2gv  2801  euind  2871  reu2  2872  reuind  2889  unissb  3766  dfiin2g  3846  tfi  4496  asymref  4924  dff13  5669  mpo2eqb  5880