Theorem 3ancoma 1045

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 466	. . 3 |- ( ( ph /\ ps ) <-> ( ps /\ ph ) )
2	1	anbi1i 731	. 2 |- ( ( ( ph /\ ps ) /\ ch ) <-> ( ( ps /\ ph ) /\ ch ) )
3		df-3an 1039	. 2 |- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ch ) )
4		df-3an 1039	. 2 |- ( ( ps /\ ph /\ ch ) <-> ( ( ps /\ ph ) /\ ch ) )
5	2, 3, 4	3bitr4i 292	1 |- ( ( ph /\ ps /\ ch ) <-> ( ps /\ ph /\ ch ) )

Syntax hints:   <-> wb 196   /\ wa 384   /\ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  3ancomb  1047  3anrev  1049  3anan12  1051  3com12  1269  cadcomb  1552  f13dfv  6530  suppssfifsupp  8290  elfzmlbp  12450  elfzo2  12473  pythagtriplem2  15522  pythagtrip  15539  xpsfrnel  16223  fucinv  16633  setcinv  16740  xrsdsreclb  19793  ordthaus  21188  regr1lem2  21543  xmetrtri2  22161  clmvscom  22890  hlcomb  25498  nb3grpr2  26285  nb3gr2nb  26286  rusgrnumwwlkslem  26864  ablomuldiv  27406  nvscom  27484  cnvadj  28751  iocinif  29543  fzto1st  29853  psgnfzto1st  29855  bnj312  30778  cgr3permute1  32155  lineext  32183  colinbtwnle  32225  outsideofcom  32235  linecom  32257  linerflx2  32258  eldmqsres  34051  cdlemg33d  35997  uunT12p3  39029  rngcinv  41981  rngcinvALTV  41993  ringcinv  42032  ringcinvALTV  42056