Theorem 19.26 1067

Description: Theorem 19.26 of [Margaris] p. 90. Also Theorem *10.22 of [WhiteheadRussell] p. 119.

Assertion

Ref	Expression
19.26	|- (A.x(ph /\ ps) <-> (A.xph /\ A.xps))

Proof of Theorem 19.26

Step	Hyp	Ref	Expression
1		pm3.26 319	. . . 4 |- ((ph /\ ps) -> ph)
2	1	19.20i 992	. . 3 |- (A.x(ph /\ ps) -> A.xph)
3		pm3.27 323	. . . 4 |- ((ph /\ ps) -> ps)
4	3	19.20i 992	. . 3 |- (A.x(ph /\ ps) -> A.xps)
5	2, 4	jca 288	. 2 |- (A.x(ph /\ ps) -> (A.xph /\ A.xps))
6		pm3.2 283	. . . 4 |- (ph -> (ps -> (ph /\ ps)))
7	6	19.20ii 995	. . 3 |- (A.xph -> (A.xps -> A.x(ph /\ ps)))
8	7	imp 350	. 2 |- ((A.xph /\ A.xps) -> A.x(ph /\ ps))
9	5, 8	impbi 157	1 |- (A.x(ph /\ ps) <-> (A.xph /\ A.xps))

Syntax hints:   <-> wb 146   /\ wa 223  A.wal 954

This theorem is referenced by:  19.26-2 1068  19.27 1069  19.28 1070  19.35 1075  19.43 1088  albi 1107  2albi 1108  hband 1111  a4imed 1161  ax11eq 1363  ax11el 1364  a12stdy2 1373  a12lem1 1376  2eu4 1452  bm1.1 1462  r19.26 1749  r19.26m 1751  unss 2202  ralpr 2426  prsspw 2478  intun 2560  intpr 2561  bm1.3ii 2704  relop 3273  asymref2 3438  dfer2 4260  suppsr3 5212  pre-axsup 5279  spwpr2 8615  axgroth4 8735  grothprim 8738

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-4 973  ax-5o 975

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain