Theorem 19.26 1108

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 326	. . . 4 |- ((ph /\ ps) -> ph)
2	1	19.20i 1033	. . 3 |- (A.x(ph /\ ps) -> A.xph)
3		pm3.27 330	. . . 4 |- ((ph /\ ps) -> ps)
4	3	19.20i 1033	. . 3 |- (A.x(ph /\ ps) -> A.xps)
5	2, 4	jca 295	. 2 |- (A.x(ph /\ ps) -> (A.xph /\ A.xps))
6		pm3.2 290	. . . 4 |- (ph -> (ps -> (ph /\ ps)))
7	6	19.20ii 1036	. . 3 |- (A.xph -> (A.xps -> A.x(ph /\ ps)))
8	7	imp 357	. 2 |- ((A.xph /\ A.xps) -> A.x(ph /\ ps))
9	5, 8	impbii 164	1 |- (A.x(ph /\ ps) <-> (A.xph /\ A.xps))

Syntax hints:   <-> wb 153   /\ wa 230  A.wal 995

This theorem is referenced by:  19.26-2 1109  19.27 1110  19.28 1111  19.35 1116  19.43 1129  albi 1148  2albi 1149  hband 1152  a4imed 1203  ax11eq 1405  ax11el 1406  a12stdy2 1415  a12lem1 1418  2eu4 1495  bm1.1 1508  r19.26 1797  r19.26m 1799  unss 2255  ralpr 2480  prsspw 2534  intun 2616  intpr 2617  bm1.3ii 2761  relop 3332  asymref2 3497  dfer2 4320  suppsr3 5289  pre-axsup 5356  spwpr2 8742  axgroth4 8863  grothprim 8866  usinuniop 10703

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1004  ax-4 1014  ax-5o 1016

This theorem depends on definitions:  df-bi 154  df-an 232

Copyright terms: Public domain