Theorem 19.26 1474

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 108	. . . 4 |- ( ( ph /\ ps ) -> ph )
2	1	alimi 1448	. . 3 |- ( A. x ( ph /\ ps ) -> A. x ph )
3		simpr 109	. . . 4 |- ( ( ph /\ ps ) -> ps )
4	3	alimi 1448	. . 3 |- ( A. x ( ph /\ ps ) -> A. x ps )
5	2, 4	jca 304	. 2 |- ( A. x ( ph /\ ps ) -> ( A. x ph /\ A. x ps ) )
6		id 19	. . 3 |- ( ( ph /\ ps ) -> ( ph /\ ps ) )
7	6	alanimi 1452	. 2 |- ( ( A. x ph /\ A. x ps ) -> A. x ( ph /\ ps ) )
8	5, 7	impbii 125	1 |- ( A. x ( ph /\ ps ) <-> ( A. x ph /\ A. x ps ) )

Syntax hints:   /\ wa 103   <-> wb 104   A.wal 1346

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  19.26-2  1475  19.26-3an  1476  albiim  1480  2albiim  1481  hband  1482  hban  1540  19.27h  1553  19.27  1554  19.28h  1555  19.28  1556  nford  1560  nfand  1561  equsexd  1722  equveli  1752  sbanv  1882  2eu4  2112  bm1.1  2155  r19.26m  2601  unss  3301  ralunb  3308  ssin  3349  intun  3862  intpr  3863  eqrelrel  4712  relop  4761  eqoprab2b  5911  dfer2  6514  omniwomnimkv  7143