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

Theorem 3ancoma 943
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 438 . . 3  |-  ( (
ph  /\  ps )  <->  ( ps  /\  ph )
)
21anbi1i 677 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  <->  ( ( ps  /\  ph )  /\  ch ) )
3 df-3an 938 . 2  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ( ph  /\  ps )  /\  ch )
)
4 df-3an 938 . 2  |-  ( ( ps  /\  ph  /\  ch )  <->  ( ( ps 
/\  ph )  /\  ch ) )
52, 3, 43bitr4i 269 1  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ps  /\  ph  /\ 
ch ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    /\ wa 359    /\ w3a 936
This theorem is referenced by:  3ancomb  945  3anrev  947  3anan12  949  3com12  1157  elfzo2  11135  pythagtriplem2  13183  pythagtrip  13200  xpsfrnel  13780  fucinv  14162  setcinv  14237  xrsdsreclb  16737  ordthaus  17440  regr1lem2  17764  xmetrtri2  18378  nbgrasym  21441  nb3grapr2  21455  nb3gra2nb  21456  ablomuldiv  21869  nvadd12  22094  nvscom  22102  cnvadj  23387  iocinif  24136  cgr3permute1  25974  lineext  26002  colinbtwnle  26044  outsideofcom  26054  linecom  26076  linerflx2  26077  f13dfv  28057  elfzmlbp  28081  frgra3v  28319  uunT12p3  28841  bnj312  29003  cdlemg33d  31433
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator