Theorem 19.26 749

Description: Theorem 19.26 of [Margaris] p. 90.

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 256	. . . 4 |- ((ph /\ ps) -> ph)
2	1	19.20i 691	. . 3 |- (A.x(ph /\ ps) -> A.xph)
3		pm3.27 260	. . . 4 |- ((ph /\ ps) -> ps)
4	3	19.20i 691	. . 3 |- (A.x(ph /\ ps) -> A.xps)
5	2, 4	jca 236	. 2 |- (A.x(ph /\ ps) -> (A.xph /\ A.xps))
6		pm3.2 232	. . . 4 |- (ph -> (ps -> (ph /\ ps)))
7	6	19.20ii 692	. . 3 |- (A.xph -> (A.xps -> A.x(ph /\ ps)))
8	7	imp 277	. 2 |- ((A.xph /\ A.xps) -> A.x(ph /\ ps))
9	5, 8	impbi 139	1 |- (A.x(ph /\ ps) <-> (A.xph /\ A.xps))

Syntax hints:   <-> wb 127   /\ wa 196  A.wal 672

This theorem is referenced by:  19.27 750  19.28 751  19.35 754  19.43 767  albi 785  hband 788  a4c1 844  2eu4 1070  bm1.1 1088  r19.26 1289  r19.26m 1291  bm1.3ii 1481  unss 1632  prsspw 1858  intun 1989  intpr 1990  cleqrel 2483  er2 3201  suppsr3 4018  axsup 4088

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-gen 677

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org