Theorem alcom 1034

Description: Theorem 19.5 of [Margaris] p. 89.

Assertion

Ref	Expression
alcom	|- (A.xA.yph <-> A.yA.xph)

Proof of Theorem alcom

Step	Hyp	Ref	Expression
1		ax-7 964	. 2 |- (A.xA.yph -> A.yA.xph)
2		ax-7 964	. 2 |- (A.yA.xph -> A.xA.yph)
3	1, 2	impbi 157	1 |- (A.xA.yph <-> A.yA.xph)

Syntax hints:   <-> wb 146  A.wal 956

This theorem is referenced by:  alrot4 1099  sbcom 1260  sbcom2 1336  sbal2 1360  2mo 1450  2eu4 1455  ralcom 1777  unissb 2532  dfiin2 2592  iunss 2595  ssiin 2603  dftr5 2688  cotr 3442  cnvsym 3443  dffun2 3532  fun11 3568  f1fv 3880  aceq1 4739

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964

This theorem depends on definitions:  df-bi 147

Copyright terms: Public domain