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

Theorem 3ancoma 972
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 967 . 2  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ( ph  /\  ps )  /\  ch )
)
4 df-3an 967 . 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 965
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 967
This theorem is referenced by:  3ancomb  974  3anrev  976  3anan12  978  3com12  1192  suppssfifsupp  7733  elfzmlbp  11589  elfzo2  11654  pythagtriplem2  13983  pythagtrip  14000  xpsfrnel  14600  fucinv  14982  setcinv  15057  xrsdsreclb  17966  ordthaus  19101  regr1lem2  19426  xmetrtri2  20044  nbgrasym  23480  nb3grapr2  23494  nb3gra2nb  23495  ablomuldiv  23908  nvadd12  24133  nvscom  24141  cnvadj  25428  iocinif  26202  cgr3permute1  28210  lineext  28238  colinbtwnle  28280  outsideofcom  28290  linecom  28312  linerflx2  28313  f13dfv  30282  iswwlk  30452  rusgranumwlklem0  30701  frgra3v  30729  uunT12p3  31832  bnj312  31997  cdlemg33d  34656
  Copyright terms: Public domain W3C validator