Theorem alcom 1028

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 959	. 2 |- (A.xA.yph -> A.yA.xph)
2		ax-7 959	. 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 951

This theorem is referenced by:  alrot4 1093  sbcom 1253  sbcom2 1329  sbal2 1351  2mo 1440  2eu4 1445  ralcom 1766  unissb 2518  dfiin2 2578  iunss 2581  ssiin 2589  dftr5 2673  cotr 3420  cnvsym 3421  dffun2 3512  fun11 3548  f1fv 3859  aceq1 4701

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

This theorem depends on definitions:  df-bi 147

Copyright terms: Public domain