Theorem 19.21v 1873

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 1583 via the use of distinct variable conditions combined with ax-17 1526. 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 2031 derived from df-eu 2029. 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 1526	. 2 |- ( ph -> A. x ph )
2	1	19.21h 1557	1 |- ( A. x ( ph -> ps ) <-> ( ph -> A. x ps ) )

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ial 1534  ax-i5r 1535

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm11.53  1895  cbval2  1921  sbhb  1940  2sb6  1984  sbcom2v  1985  2sb6rf  1990  2exsb  2009  moanim  2100  r3al  2521  ceqsralt  2766  rspc2gv  2855  euind  2926  reu2  2927  reuind  2944  unissb  3841  dfiin2g  3921  tfi  4583  asymref  5016  dff13  5771  mpo2eqb  5986