Theorem 19.26 1530

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

Assertion

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

Proof of Theorem 19.26

Step	Hyp	Ref	Expression
1		simpl 109	. . . 4 |- ( ( ph /\ ps ) -> ph )
2	1	alimi 1504	. . 3 |- ( A. x ( ph /\ ps ) -> A. x ph )
3		simpr 110	. . . 4 |- ( ( ph /\ ps ) -> ps )
4	3	alimi 1504	. . 3 |- ( A. x ( ph /\ ps ) -> A. x ps )
5	2, 4	jca 306	. 2 |- ( A. x ( ph /\ ps ) -> ( A. x ph /\ A. x ps ) )
6		id 19	. . 3 |- ( ( ph /\ ps ) -> ( ph /\ ps ) )
7	6	alanimi 1508	. 2 |- ( ( A. x ph /\ A. x ps ) -> A. x ( ph /\ ps ) )
8	5, 7	impbii 126	1 |- ( A. x ( ph /\ ps ) <-> ( A. x ph /\ A. x ps ) )

Syntax hints:   /\ wa 104   <-> wb 105   A.wal 1396

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1496  ax-gen 1498

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  19.26-2  1531  19.26-3an  1532  albiim  1536  2albiim  1537  hband  1538  hban  1596  19.27h  1609  19.27  1610  19.28h  1611  19.28  1612  nford  1616  nfand  1617  equsexd  1778  equveli  1808  sbanv  1940  2eu4  2176  bm1.1  2219  r19.26m  2676  unss  3397  ralunb  3404  ssin  3447  intun  3985  intpr  3986  eqrelrel  4856  relop  4910  eqoprab2b  6119  dfer2  6781  omniwomnimkv  7471