Theorem 19.26 1504

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 1478	. . 3 |- ( A. x ( ph /\ ps ) -> A. x ph )
3		simpr 110	. . . 4 |- ( ( ph /\ ps ) -> ps )
4	3	alimi 1478	. . 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 1482	. 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 1371

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 1470  ax-gen 1472

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  19.26-2  1505  19.26-3an  1506  albiim  1510  2albiim  1511  hband  1512  hban  1570  19.27h  1583  19.27  1584  19.28h  1585  19.28  1586  nford  1590  nfand  1591  equsexd  1752  equveli  1782  sbanv  1913  2eu4  2147  bm1.1  2190  r19.26m  2637  unss  3347  ralunb  3354  ssin  3395  intun  3916  intpr  3917  eqrelrel  4776  relop  4828  eqoprab2b  6003  dfer2  6621  omniwomnimkv  7269