Theorem 19.26 1505

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 1479	. . 3 |- ( A. x ( ph /\ ps ) -> A. x ph )
3		simpr 110	. . . 4 |- ( ( ph /\ ps ) -> ps )
4	3	alimi 1479	. . 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 1483	. 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 1471  ax-gen 1473

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  19.26-2  1506  19.26-3an  1507  albiim  1511  2albiim  1512  hband  1513  hban  1571  19.27h  1584  19.27  1585  19.28h  1586  19.28  1587  nford  1591  nfand  1592  equsexd  1753  equveli  1783  sbanv  1914  2eu4  2149  bm1.1  2192  r19.26m  2639  unss  3355  ralunb  3362  ssin  3403  intun  3930  intpr  3931  eqrelrel  4794  relop  4846  eqoprab2b  6026  dfer2  6644  omniwomnimkv  7295