Theorem 19.26 1530

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 1504	. . 3 |- ( A. x ( ph /\ ps ) -> A. x ph )
3		simpr 110	. . . 4 |- ( ( ph /\ ps ) -> ps )
4	3	alimi 1504	. . 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 1508	. 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 1396

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 1496  ax-gen 1498

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  19.26-2  1531  19.26-3an  1532  albiim  1536  2albiim  1537  hband  1538  hban  1596  19.27h  1609  19.27  1610  19.28h  1611  19.28  1612  nford  1616  nfand  1617  equsexd  1778  equveli  1808  sbanv  1940  2eu4  2176  bm1.1  2219  r19.26m  2676  unss  3395  ralunb  3402  ssin  3445  intun  3982  intpr  3983  eqrelrel  4853  relop  4907  eqoprab2b  6113  dfer2  6770  omniwomnimkv  7460