Theorem prcom 4108

Description: Commutative law for unordered pairs. (Contributed by NM, 15-Jul-1993.)

Assertion

Ref	Expression
prcom

Proof of Theorem prcom

Step	Hyp	Ref	Expression
1		uncom 3647	. 2
2		df-pr 4032	. 2
3		df-pr 4032	. 2
4	1, 2, 3	3eqtr4i 2496	1

Syntax hints:  =wceq 1395  u.cun 3473  {csn 4029  {cpr 4031

This theorem is referenced by:  preq2  4110  tpcoma  4126  tpidm23  4133  prid2g  4137  prid2  4139  prprc2  4141  difprsn2  4167  tpprceq3  4170  tppreqb  4171  preqr2  4205  preq12b  4206  prnebg  4212  fvpr2  6115  fvpr2g  6117  en2other2  8408  hashprb  12462  joincomALT  15659  meetcomALT  15661  symggen  16495  psgnran  16540  lspprid2  17644  lspexchn2  17777  lspindp2l  17780  lspindp2  17781  lsppratlem1  17793  psgnghm  18616  uvcvvcl  18818  mdetralt  19110  mdetunilem7  19120  usgraedgprv  24376  usgraedgrnv  24377  usgra2edg  24382  usgraedg4  24387  usgraidx2vlem1  24391  usgraidx2vlem2  24392  nbgraeledg  24430  nbgrassvwo2  24438  nbgrasym  24439  nbgracnvfv  24440  nbgraf1olem3  24443  nbgraf1olem5  24445  nb3graprlem1  24451  nb3graprlem2  24452  nb3grapr  24453  nb3grapr2  24454  nb3gra2nb  24455  cusgra2v  24462  cusgra3v  24464  uvtxnbgra  24493  uvtxnb  24497  2trllemH  24554  2trllemE  24555  wlkntrllem2  24562  usgrcyclnl2  24641  4cycl4dv  24667  cusconngra  24676  clwwlkn2  24775  vdgr1c  24905  vdegp1ci  24986  frgraunss  24995  frisusgranb  24997  frgra3v  25002  3vfriswmgra  25005  1to3vfriswmgra  25007  1to3vfriendship  25008  2pthfrgrarn  25009  2pthfrgra  25011  3cyclfrgrarn1  25012  4cycl2v2nb  25016  n4cyclfrgra  25018  frgranbnb  25020  frgrancvvdeqlem2  25031  frgrancvvdeqlem4  25033  frgrancvvdeqlem7  25036  frgrawopreglem4  25047  frgrawopreg  25049  frgrawopreg2  25051  frg2woteqm  25059  usg2spot2nb  25065  numclwwlkovf2ex  25086  indf  28029  indpreima  28038  measxun2  28181  measssd  28186  usgra2pthlem1  32353  usgvincvad  32404  usgvincvadALT  32407  usgedgvadf1lem1  32413  usgedgvadf1lem2  32414  usgedgvadf1ALTlem1  32416  usgedgvadf1ALTlem2  32417  dihprrn  37153  dvh3dim  37173  dvh3dim3N  37176  lcfrlem21  37290  mapdindp4  37450  mapdh6eN  37467  mapdh7dN  37477  mapdh8ab  37504  mapdh8ad  37506  mapdh8b  37507  mapdh8e  37511  hdmap1l6e  37542  hdmap11lem2  37572

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-un 3480  df-pr 4032