Theorem 19.26 1063

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 989	. . 3 |- (A.x(ph /\ ps) -> A.xph)
3		pm3.27 323	. . . 4 |- ((ph /\ ps) -> ps)
4	3	19.20i 989	. . 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 992	. . 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 951

This theorem is referenced by:  19.26-2 1064  19.27 1065  19.28 1066  19.35 1071  19.43 1084  albi 1103  2albi 1104  hband 1107  a4imed 1157  ax11eq 1356  ax11el 1357  a12stdy2 1366  a12lem1 1369  2eu4 1445  bm1.1 1455  r19.26 1742  r19.26m 1744  unss 2194  ralpr 2418  prsspw 2471  intun 2552  intpr 2553  bm1.3ii 2696  relop 3265  asymref2 3424  asymref2OLD 3426  dfer2 4246  suppsr3 5196  pre-axsup 5263  axgroth4 8719  grothprim 8722

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-4 970  ax-5o 972

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

Copyright terms: Public domain