Theorem 19.26 1534

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

This proof depends on syntax axioms:   /\ wa 104   <-> wb 105   A.wal 1400

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502

This proof depends on definitions:  df-bi 117

This theorem is used by:  19.26-2  1535  19.26-3an  1536  albiim  1540  2albiim  1541  hband  1542  hban  1600  19.27h  1613  19.27  1614  19.28h  1615  19.28  1616  nford  1620  nfand  1621  equsexd  1782  equveli  1812  sbanv  1944  2eu4  2180  bm1.1  2223  r19.26m  2682  unss  3403  ralunb  3410  ssin  3453  intun  4001  intpr  4002  eqrelrel  4876  relop  4930  eqoprab2b  6146  dfer2  6808  omniwomnimkv  7507  als-no-surprise  17147