Theorem 19.26 1593

Description: Theorem 19.26 of [Margaris] p. 90. Also Theorem *10.22 of [WhiteheadRussell] p. 147. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 4-Jul-2014.)

Assertion

Ref	Expression
19.26	|- (A.x(ph /\ ps) <-> (A.xph /\ A.xps))

Proof of Theorem 19.26

Step	Hyp	Ref	Expression
1		simpl 443	. . . 4 |- ((ph /\ ps) -> ph)
2	1	alimi 1559	. . 3 |- (A.x(ph /\ ps) -> A.xph)
3		simpr 447	. . . 4 |- ((ph /\ ps) -> ps)
4	3	alimi 1559	. . 3 |- (A.x(ph /\ ps) -> A.xps)
5	2, 4	jca 518	. 2 |- (A.x(ph /\ ps) -> (A.xph /\ A.xps))
6		id 19	. . 3 |- ((ph /\ ps) -> (ph /\ ps))
7	6	alanimi 1562	. 2 |- ((A.xph /\ A.xps) -> A.x(ph /\ ps))
8	5, 7	impbii 180	1 |- (A.x(ph /\ ps) <-> (A.xph /\ A.xps))

Syntax hints:   <-> wb 176   /\ wa 358  A.wal 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557

This theorem depends on definitions:  df-bi 177  df-an 360

This theorem is referenced by:  19.26-2  1594  19.26-3an  1595  19.35  1600  19.43OLD  1606  albiim  1611  2albiim  1612  19.27  1869  19.28  1870  ax12olem2  1928  ax11eq  2193  ax11el  2194  2eu4  2287  bm1.1  2338  r19.26m  2749  unss  3437  ralunb  3444  ssin  3477  intun  3958  intpr  3959  eqopr  4847