Theorem 19.26 1410

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 107	. . . 4 |- ( ( ph /\ ps ) -> ph )
2	1	alimi 1384	. . 3 |- ( A. x ( ph /\ ps ) -> A. x ph )
3		simpr 108	. . . 4 |- ( ( ph /\ ps ) -> ps )
4	3	alimi 1384	. . 3 |- ( A. x ( ph /\ ps ) -> A. x ps )
5	2, 4	jca 300	. 2 |- ( A. x ( ph /\ ps ) -> ( A. x ph /\ A. x ps ) )
6		id 19	. . 3 |- ( ( ph /\ ps ) -> ( ph /\ ps ) )
7	6	alanimi 1388	. 2 |- ( ( A. x ph /\ A. x ps ) -> A. x ( ph /\ ps ) )
8	5, 7	impbii 124	1 |- ( A. x ( ph /\ ps ) <-> ( A. x ph /\ A. x ps ) )

Syntax hints:   /\ wa 102   <-> wb 103   A.wal 1282

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  19.26-2  1411  19.26-3an  1412  albiim  1416  2albiim  1417  hband  1418  hban  1479  19.27h  1492  19.27  1493  19.28h  1494  19.28  1495  nford  1499  nfand  1500  equsexd  1657  equveli  1682  sbanv  1810  2eu4  2034  bm1.1  2066  r19.26m  2488  unss  3146  ralunb  3153  ssin  3188  intun  3667  intpr  3668  eqrelrel  4459  relop  4504  eqoprab2b  5583  dfer2  6130