MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3ancoma 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  11075  pythagtriplem2  13120  pythagtrip  13137  xpsfrnel  13717  fucinv  14099  setcinv  14174  xrsdsreclb  16670  ordthaus  17372  regr1lem2  17695  xmetrtri2  18296  nbgrasym  21317  nb3grapr2  21331  nb3gra2nb  21332  ablomuldiv  21727  nvadd12  21952  nvscom  21960  cnvadj  23245  iocinif  23982  cgr3permute1  25698  lineext  25726  colinbtwnle  25768  outsideofcom  25778  linecom  25800  linerflx2  25801  frgra3v  27757  uunT12p3  28257  bnj312  28416  cdlemg33d  30825
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