Theorem 19.26 1370

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 102	. . . 4 |- ( ( ph /\ ps ) -> ph )
2	1	alimi 1344	. . 3 |- ( A. x ( ph /\ ps ) -> A. x ph )
3		simpr 103	. . . 4 |- ( ( ph /\ ps ) -> ps )
4	3	alimi 1344	. . 3 |- ( A. x ( ph /\ ps ) -> A. x ps )
5	2, 4	jca 290	. 2 |- ( A. x ( ph /\ ps ) -> ( A. x ph /\ A. x ps ) )
6		id 19	. . 3 |- ( ( ph /\ ps ) -> ( ph /\ ps ) )
7	6	alanimi 1348	. 2 |- ( ( A. x ph /\ A. x ps ) -> A. x ( ph /\ ps ) )
8	5, 7	impbii 117	1 |- ( A. x ( ph /\ ps ) <-> ( A. x ph /\ A. x ps ) )

Syntax hints:   /\ wa 97   <-> wb 98   A.wal 1241

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  19.26-2  1371  19.26-3an  1372  albiim  1376  2albiim  1377  hband  1378  hban  1439  19.27h  1452  19.27  1453  19.28h  1454  19.28  1455  nford  1459  nfand  1460  equsexd  1617  equveli  1642  sbanv  1769  2eu4  1993  bm1.1  2025  r19.26m  2444  unss  3117  ralunb  3124  ssin  3159  intun  3646  intpr  3647  eqrelrel  4441  relop  4486  eqoprab2b  5563  dfer2  6107