Theorem 19.21v 1896

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 1606 via the use of distinct variable conditions combined with ax-17 1549. 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 2059 derived from df-eu 2057. 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 1549	. 2 |- ( ph -> A. x ph )
2	1	19.21h 1580	1 |- ( A. x ( ph -> ps ) <-> ( ph -> A. x ps ) )

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 107  ax-ia3 108  ax-5 1470  ax-gen 1472  ax-4 1533  ax-17 1549  ax-ial 1557  ax-i5r 1558

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm11.53  1919  cbval2  1945  cbvaldvaw  1954  sbhb  1968  2sb6  2012  sbcom2v  2013  2sb6rf  2018  2exsb  2037  moanim  2128  r3al  2550  ceqsralt  2799  rspc2gv  2889  euind  2960  reu2  2961  reuind  2978  unissb  3880  dfiin2g  3960  tfi  4630  asymref  5068  dff13  5837  mpo2eqb  6055