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 1750  r19.26m 1752  unss 2204  ralpr 2428  prsspw 2480  intun 2562  intpr 2563  bm1.3ii 2706  relop 3275  asymref2 3440  dfer2 4262  suppsr3 5224  pre-axsup 5291  spwpr2 8658  axgroth4 8780  grothprim 8783

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