Theorem 19.21v 1926

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 1636 via the use of distinct variable conditions combined with ax-17 1579. 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 2091 derived from df-eu 2089. 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 1579	. 2 |- ( ph -> A. x ph )
2	1	19.21h 1610	1 |- ( A. x ( ph -> ps ) <-> ( ph -> A. x ps ) )

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ial 1587  ax-i5r 1588

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm11.53  1951  cbval2  1977  cbvaldvaw  1986  sbhb  2000  2sb6  2044  sbcom2v  2045  2sb6rf  2050  2exsb  2069  moanim  2161  r3al  2594  ceqsralt  2849  rspc2gv  2942  euind  3013  reu2  3014  reuind  3031  unissb  3960  dfiin2g  4040  tfi  4724  asymref  5168  dff13  5964  mpo2eqb  6188