Theorem alcom 1030

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

This theorem is referenced by:  alrot4 1095  sbcom 1256  sbcom2 1332  sbal2 1356  2mo 1445  2eu4 1450  ralcom 1771  unissb 2523  dfiin2 2583  iunss 2586  ssiin 2594  dftr5 2678  cotr 3428  cnvsym 3429  dffun2 3518  fun11 3554  f1fv 3865  aceq1 4709

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

This theorem depends on definitions:  df-bi 147

Copyright terms: Public domain