Theorem 3ancoma 975

Description: Commutation law for triple conjunction. (Contributed by NM, 21-Apr-1994.)

Assertion

Ref	Expression
3ancoma	|- ( ( ph /\ ps /\ ch ) <-> ( ps /\ ph /\ ch ) )

Proof of Theorem 3ancoma

Step	Hyp	Ref	Expression
1		ancom 450	. . 3 |- ( ( ph /\ ps ) <-> ( ps /\ ph ) )
2	1	anbi1i 695	. 2 |- ( ( ( ph /\ ps ) /\ ch ) <-> ( ( ps /\ ph ) /\ ch ) )
3		df-3an 970	. 2 |- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ch ) )
4		df-3an 970	. 2 |- ( ( ps /\ ph /\ ch ) <-> ( ( ps /\ ph ) /\ ch ) )
5	2, 3, 4	3bitr4i 277	1 |- ( ( ph /\ ps /\ ch ) <-> ( ps /\ ph /\ ch ) )

Syntax hints:   <-> wb 184   /\ wa 369   /\ w3a 968

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

This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 970

This theorem is referenced by:  3ancomb  977  3anrev  979  3anan12  981  3com12  1195  f13dfv  6159  suppssfifsupp  7833  elfzmlbp  11772  elfzo2  11789  pythagtriplem2  14189  pythagtrip  14206  xpsfrnel  14807  fucinv  15189  setcinv  15264  xrsdsreclb  18226  ordthaus  19644  regr1lem2  19969  xmetrtri2  20587  nbgrasym  24101  nb3grapr2  24116  nb3gra2nb  24117  iswwlk  24345  rusgranumwlklem0  24610  ablomuldiv  24817  nvadd12  25042  nvscom  25050  cnvadj  26337  iocinif  27110  cgr3permute1  29125  lineext  29153  colinbtwnle  29195  outsideofcom  29205  linecom  29227  linerflx2  29228  frgra3v  31720  uunT12p3  32554  bnj312  32719  cdlemg33d  35380