Theorem 3ancoma 972

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 967	. 2 |- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ch ) )
4		df-3an 967	. 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 965

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 967

This theorem is referenced by:  3ancomb  974  3anrev  976  3anan12  978  3com12  1192  suppssfifsupp  7733  elfzmlbp  11589  elfzo2  11654  pythagtriplem2  13983  pythagtrip  14000  xpsfrnel  14600  fucinv  14982  setcinv  15057  xrsdsreclb  17966  ordthaus  19101  regr1lem2  19426  xmetrtri2  20044  nbgrasym  23480  nb3grapr2  23494  nb3gra2nb  23495  ablomuldiv  23908  nvadd12  24133  nvscom  24141  cnvadj  25428  iocinif  26202  cgr3permute1  28210  lineext  28238  colinbtwnle  28280  outsideofcom  28290  linecom  28312  linerflx2  28313  f13dfv  30282  iswwlk  30452  rusgranumwlklem0  30701  frgra3v  30729  uunT12p3  31832  bnj312  31997  cdlemg33d  34656