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

Theorem 3ancoma 975
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 450 . . 3  |-  ( (
ph  /\  ps )  <->  ( ps  /\  ph )
)
21anbi1i 695 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  <->  ( ( ps  /\  ph )  /\  ch ) )
3 df-3an 970 . 2  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ( ph  /\  ps )  /\  ch )
)
4 df-3an 970 . 2  |-  ( ( ps  /\  ph  /\  ch )  <->  ( ( ps 
/\  ph )  /\  ch ) )
52, 3, 43bitr4i 277 1  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ps  /\  ph  /\ 
ch ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 369    /\ w3a 968
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 970
This theorem is referenced by:  3ancomb  977  3anrev  979  3anan12  981  3com12  1195  f13dfv  6159  suppssfifsupp  7833  elfzmlbp  11772  elfzo2  11789  pythagtriplem2  14189  pythagtrip  14206  xpsfrnel  14807  fucinv  15189  setcinv  15264  xrsdsreclb  18226  ordthaus  19644  regr1lem2  19969  xmetrtri2  20587  nbgrasym  24101  nb3grapr2  24116  nb3gra2nb  24117  iswwlk  24345  rusgranumwlklem0  24610  ablomuldiv  24817  nvadd12  25042  nvscom  25050  cnvadj  26337  iocinif  27110  cgr3permute1  29125  lineext  29153  colinbtwnle  29195  outsideofcom  29205  linecom  29227  linerflx2  29228  frgra3v  31720  uunT12p3  32554  bnj312  32719  cdlemg33d  35380
  Copyright terms: Public domain W3C validator