Theorem 19.21v 1883

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 1593 via the use of distinct variable conditions combined with ax-17 1536. 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 2041 derived from df-eu 2039. 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 1536	. 2 |- ( ph -> A. x ph )
2	1	19.21h 1567	1 |- ( A. x ( ph -> ps ) <-> ( ph -> A. x ps ) )

Syntax hints:   -> wi 4   <-> wb 105   A.wal 1361

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 107  ax-ia3 108  ax-5 1457  ax-gen 1459  ax-4 1520  ax-17 1536  ax-ial 1544  ax-i5r 1545

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm11.53  1905  cbval2  1931  sbhb  1950  2sb6  1994  sbcom2v  1995  2sb6rf  2000  2exsb  2019  moanim  2110  r3al  2531  ceqsralt  2776  rspc2gv  2865  euind  2936  reu2  2937  reuind  2954  unissb  3851  dfiin2g  3931  tfi  4593  asymref  5026  dff13  5782  mpo2eqb  5997