Theorem alcom 1073

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 1003	. 2 |- (A.xA.yph -> A.yA.xph)
2		ax-7 1003	. 2 |- (A.yA.xph -> A.xA.yph)
3	1, 2	impbii 164	1 |- (A.xA.yph <-> A.yA.xph)

Syntax hints:   <-> wb 153  A.wal 995

This theorem is referenced by:  alrot4 1138  sbcom 1300  sbcom2 1376  sbal2 1400  2mo 1490  2eu4 1495  ralcom 1821  unissb 2582  dfiin2 2642  iunss 2645  ssiin 2653  dftr5 2738  cotr 3493  cnvsym 3494  dffun2 3583  fun11 3619  f1fv 3931  aceq1 4791

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

This theorem depends on definitions:  df-bi 154

Copyright terms: Public domain