Theorem alcom 1379

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

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

This theorem is referenced by:  alrot4 1451  sbcom 1632  sbcom2 1724  sbal2 1749  2mo 1851  2eu4 1856  ralcom 2242  unissb 3208  dfiin2g 3286  dfiin2OLD 3288  iunssOLD 3292  ssiinOLD 3303  dftr5 3414  euexeqOLD 3826  euexaleq 3827  cotr 4302  cotrOLD 4303  cnvsym 4304  cnvsymOLD 4305  dffun2 4431  fun11 4480  dff13 4850  aceq1 5891  dfon2lem8 13856  dfiin2gOLD 15356  alrot3 16325

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

This theorem depends on definitions:  df-bi 164

Copyright terms: Public domain