MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3ancoma Unicode version

Theorem 3ancoma 941
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
StepHypRef Expression
1 ancom 437 . . 3  |-  ( (
ph  /\  ps )  <->  ( ps  /\  ph )
)
21anbi1i 676 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  <->  ( ( ps  /\  ph )  /\  ch ) )
3 df-3an 936 . 2  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ( ph  /\  ps )  /\  ch )
)
4 df-3an 936 . 2  |-  ( ( ps  /\  ph  /\  ch )  <->  ( ( ps 
/\  ph )  /\  ch ) )
52, 3, 43bitr4i 268 1  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ps  /\  ph  /\ 
ch ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358    /\ w3a 934
This theorem is referenced by:  3ancomb  943  3anrev  945  3anan12  947  3com12  1155  elfzo2  10878  pythagtriplem2  12870  pythagtrip  12887  xpsfrnel  13465  fucinv  13847  setcinv  13922  xrsdsreclb  16418  ordthaus  17112  regr1lem2  17431  xmetrtri2  17920  ablomuldiv  20956  nvadd12  21179  nvscom  21187  cnvadj  22472  iocinif  23274  cgr3permute1  24671  lineext  24699  colinbtwnle  24741  outsideofcom  24751  linecom  24773  linerflx2  24774  issubcata  25846  nbgrasym  28152  frgra3v  28180  uunT12p3  28577  bnj312  28737  cdlemg33d  30898
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator