Theorem 19.21 1403

Description: Theorem 19.21 of [Margaris] p. 90. The hypothesis can be thought of as "x is not free in ph."

Hypothesis

Ref	Expression
19.21.1	|- (ph -> A.xph)

Assertion

Ref	Expression
19.21	|- (A.x(ph -> ps) <-> (ph -> A.xps))

Proof of Theorem 19.21

Step	Hyp	Ref	Expression
1		alim 1340	. . 3 |- (A.x(ph -> ps) -> (A.xph -> A.xps))
2		19.21.1	. . 3 |- (ph -> A.xph)
3	1, 2	syl5 20	. 2 |- (A.x(ph -> ps) -> (ph -> A.xps))
4		hba1 1350	. . . 4 |- (A.xps -> A.xA.xps)
5	2, 4	hbim 1354	. . 3 |- ((ph -> A.xps) -> A.x(ph -> A.xps))
6		ax-4 1319	. . . 4 |- (A.xps -> ps)
7	6	imim2i 11	. . 3 |- ((ph -> A.xps) -> (ph -> ps))
8	5, 7	19.21ai 1345	. 2 |- ((ph -> A.xps) -> A.x(ph -> ps))
9	3, 8	impbii 174	1 |- (A.x(ph -> ps) <-> (ph -> A.xps))

Syntax hints:   -> wi 3   <-> wb 163  A.wal 1296

This theorem is referenced by:  19.21-2 1404  stdpc5 1405  19.32 1438  hbim1 1458  19.21v 1663  19.12vv 1681  cbvaldOLD 1703  ax15 1750  eu2 1791  moanim 1826  bnj584 12550  bnj585 12551  bnj870 12798  19.12b 13868  ax12 16367

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-4 1319  ax-5o 1321  ax-6o 1324

This theorem depends on definitions:  df-bi 164

Copyright terms: Public domain