Theorem 19.21v 1861

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 1571 via the use of distinct variable conditions combined with ax-17 1514. 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 2019 derived from df-eu 2017. 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 1514	. 2 |- ( ph -> A. x ph )
2	1	19.21h 1545	1 |- ( A. x ( ph -> ps ) <-> ( ph -> A. x ps ) )

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-4 1498  ax-17 1514  ax-ial 1522  ax-i5r 1523

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm11.53  1883  cbval2  1909  sbhb  1928  2sb6  1972  sbcom2v  1973  2sb6rf  1978  2exsb  1997  moanim  2088  r3al  2510  ceqsralt  2753  rspc2gv  2842  euind  2913  reu2  2914  reuind  2931  unissb  3819  dfiin2g  3899  tfi  4559  asymref  4989  dff13  5736  mpo2eqb  5951