Theorem albi 1344

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

Assertion

Ref	Expression
albi	|- (A.x(ph <-> ps) -> (A.xph <-> A.xps))

Proof of Theorem albi

Step	Hyp	Ref	Expression
1		bi1 165	. . 3 |- ((ph <-> ps) -> (ph -> ps))
2	1	al2imi 1341	. 2 |- (A.x(ph <-> ps) -> (A.xph -> A.xps))
3		bi2 166	. . 3 |- ((ph <-> ps) -> (ps -> ph))
4	3	al2imi 1341	. 2 |- (A.x(ph <-> ps) -> (A.xps -> A.xph))
5	2, 4	impbid 574	1 |- (A.x(ph <-> ps) -> (A.xph <-> A.xps))

Syntax hints:   -> wi 3   <-> wb 163  A.wal 1296

This theorem is referenced by:  albii 1346  19.16 1395  19.17 1396  19.33b 1444  19.33bOLD 1445  albid 1459  intmin4 3246  dfiin2g 3286  bnj1155 12947  dfiin2gOLD 15356  2albi 16330  ralbidar 16422  hbra2VD 16684  trsbcVD 16701

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-4 1319  ax-5o 1321

This theorem depends on definitions:  df-bi 164  df-an 242

Copyright terms: Public domain