Theorem 3ancoma 981

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 448	. . 3 |- ( ( ph /\ ps ) <-> ( ps /\ ph ) )
2	1	anbi1i 693	. 2 |- ( ( ( ph /\ ps ) /\ ch ) <-> ( ( ps /\ ph ) /\ ch ) )
3		df-3an 976	. 2 |- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ch ) )
4		df-3an 976	. 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 367   /\ w3a 974

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 369  df-3an 976

This theorem is referenced by:  3ancomb  983  3anrev  985  3anan12  987  3com12  1201  cadcomb  1480  f13dfv  6161  suppssfifsupp  7878  elfzmlbp  11841  elfzo2  11862  pythagtriplem2  14550  pythagtrip  14567  xpsfrnel  15177  fucinv  15586  setcinv  15693  xrsdsreclb  18785  ordthaus  20178  regr1lem2  20533  xmetrtri2  21151  hlcomb  24371  nbgrasym  24856  nb3grapr2  24871  nb3gra2nb  24872  iswwlk  25100  rusgranumwlklem0  25365  frgra3v  25419  ablomuldiv  25705  nvadd12  25930  nvscom  25938  cnvadj  27224  iocinif  28040  bnj312  29091  cgr3permute1  30386  lineext  30414  colinbtwnle  30456  outsideofcom  30466  linecom  30488  linerflx2  30489  cdlemg33d  33728  uunT12p3  36623  rngcinv  38300  rngcinvALTV  38312  ringcinv  38351  ringcinvALTV  38375