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  10894  pythagtriplem2  12886  pythagtrip  12903  xpsfrnel  13481  fucinv  13863  setcinv  13938  xrsdsreclb  16434  ordthaus  17128  regr1lem2  17447  xmetrtri2  17936  ablomuldiv  20972  nvadd12  21195  nvscom  21203  cnvadj  22488  iocinif  23289  cgr3permute1  24743  lineext  24771  colinbtwnle  24813  outsideofcom  24823  linecom  24845  linerflx2  24846  issubcata  25949  nbgrasym  28286  nb3grapr2  28290  nb3gra2nb  28291  frgra3v  28426  uunT12p3  28891  bnj312  29053  cdlemg33d  31520
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