Theorem excom 1551

Description: Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
excom	|- (E.xE.yph <-> E.yE.xph)

Proof of Theorem excom

Step	Hyp	Ref	Expression
1		excomim 1550	. 2 |- (E.xE.yph -> E.yE.xph)
2		excomim 1550	. 2 |- (E.yE.xph -> E.xE.yph)
3	1, 2	impbii 117	1 |- (E.xE.yph <-> E.yE.xph)

Syntax hints:   <-> wb 98  E.wex 1378

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-4 1397  ax-ial 1424

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  excom13  1576  exrot3  1577  ee4anv  1806  sbexyz  1876  2exsb  1882  2euex  1984  2exeu  1989  2eu4  1990  rexcomf  2466  gencbvex  2594  euxfr2dc  2720  euind  2722  sbccomlem  2826  opelopabsbALT  3987  uniuni  4149  elvvv  4346  dmuni  4488  dm0rn0  4495  dmmrnm  4497  dmcosseq  4546  elres  4589  rnco  4770  coass  4782  oprabid  5480  dfoprab2  5494  opabex3d  5690  opabex3  5691  domen  6168  xpassen  6240  prarloc  6486