Theorem 19.3r 714

Description: A wff may be quantified with a variable not free in it.

Hypothesis

Ref	Expression
19.3r.1	|- (ph -> A.xph)

Assertion

Ref	Expression
19.3r	|- (ph <-> A.xph)

Proof of Theorem 19.3r

Step	Hyp	Ref	Expression
1		19.3r.1	. 2 |- (ph -> A.xph)
2		ax-4 673	. 2 |- (A.xph -> ph)
3	1, 2	impbi 139	1 |- (ph <-> A.xph)

Syntax hints:   -> wi 2   <-> wb 127  A.wal 672

This theorem is referenced by:  19.16 730  19.17 731  19.27 750  19.28 751  19.37 759  eqsal 833  2eu4 1070  kmlem14 3593  zfcndrep 3760  zfcndpow 3762  zfcndac 3765

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673

This theorem depends on definitions:  df-bi 128

metamath.org