Theorem 19.26 1469

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 1443	. . 3 |- ( A. x ( ph /\ ps ) -> A. x ph )
3		simpr 109	. . . 4 |- ( ( ph /\ ps ) -> ps )
4	3	alimi 1443	. . 3 |- ( A. x ( ph /\ ps ) -> A. x ps )
5	2, 4	jca 304	. 2 |- ( A. x ( ph /\ ps ) -> ( A. x ph /\ A. x ps ) )
6		id 19	. . 3 |- ( ( ph /\ ps ) -> ( ph /\ ps ) )
7	6	alanimi 1447	. 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 1341

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  19.26-2  1470  19.26-3an  1471  albiim  1475  2albiim  1476  hband  1477  hban  1535  19.27h  1548  19.27  1549  19.28h  1550  19.28  1551  nford  1555  nfand  1556  equsexd  1717  equveli  1747  sbanv  1877  2eu4  2107  bm1.1  2150  r19.26m  2597  unss  3296  ralunb  3303  ssin  3344  intun  3855  intpr  3856  eqrelrel  4705  relop  4754  eqoprab2b  5900  dfer2  6502  omniwomnimkv  7131