Theorem 19.26 1440

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 108	. . . 4 |- ( ( ph /\ ps ) -> ph )
2	1	alimi 1414	. . 3 |- ( A. x ( ph /\ ps ) -> A. x ph )
3		simpr 109	. . . 4 |- ( ( ph /\ ps ) -> ps )
4	3	alimi 1414	. . 3 |- ( A. x ( ph /\ ps ) -> A. x ps )
5	2, 4	jca 302	. 2 |- ( A. x ( ph /\ ps ) -> ( A. x ph /\ A. x ps ) )
6		id 19	. . 3 |- ( ( ph /\ ps ) -> ( ph /\ ps ) )
7	6	alanimi 1418	. 2 |- ( ( A. x ph /\ A. x ps ) -> A. x ( ph /\ ps ) )
8	5, 7	impbii 125	1 |- ( A. x ( ph /\ ps ) <-> ( A. x ph /\ A. x ps ) )

Syntax hints:   /\ wa 103   <-> wb 104   A.wal 1312

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-gen 1408

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  19.26-2  1441  19.26-3an  1442  albiim  1446  2albiim  1447  hband  1448  hban  1509  19.27h  1522  19.27  1523  19.28h  1524  19.28  1525  nford  1529  nfand  1530  equsexd  1690  equveli  1715  sbanv  1843  2eu4  2068  bm1.1  2100  r19.26m  2537  unss  3216  ralunb  3223  ssin  3264  intun  3768  intpr  3769  eqrelrel  4600  relop  4649  eqoprab2b  5783  dfer2  6384