Theorem 19.21v 1794

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 1515 via the use of distinct variable conditions combined with ax-17 1459. 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 1946 derived from df-eu 1944. 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 1459	. 2 |- ( ph -> A. x ph )
2	1	19.21h 1489	1 |- ( A. x ( ph -> ps ) <-> ( ph -> A. x ps ) )

Syntax hints:   -> wi 4   <-> wb 103   A.wal 1282

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378  ax-4 1440  ax-17 1459  ax-ial 1467  ax-i5r 1468

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  pm11.53  1816  cbval2  1837  sbhb  1857  2sb6  1901  sbcom2v  1902  2sb6rf  1907  2exsb  1926  moanim  2015  r3al  2408  ceqsralt  2626  rspc2gv  2712  euind  2779  reu2  2780  reuind  2795  unissb  3631  dfiin2g  3711  tfi  4323  asymref  4730  dff13  5428  mpt22eqb  5630