Theorem 19.26 1043

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

This theorem is referenced by:  19.26-2 1044  19.27 1045  19.28 1046  19.35 1051  19.43 1064  albi 1083  2albi 1084  hband 1087  a4c1 1144  ax11eq 1340  ax11el 1341  a12stdy2 1350  a12lem1 1353  2eu4 1429  bm1.1 1439  r19.26 1726  r19.26m 1728  unss 2175  ralpr 2399  prsspw 2450  intun 2530  intpr 2531  bm1.3ii 2674  er2 4200  suppsr3 5147  pre-axsup 5214  axgroth4 8632  grothprim 8635

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-gen 955

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

Copyright terms: Public domain