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

Theorem 3ancomb 946
Description: Commutation law for triple conjunction. (Contributed by NM, 21-Apr-1994.)
Assertion
Ref Expression
3ancomb  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ph  /\  ch  /\ 
ps ) )

Proof of Theorem 3ancomb
StepHypRef Expression
1 3ancoma 944 . 2  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ps  /\  ph  /\ 
ch ) )
2 3anrot 942 . 2  |-  ( ( ps  /\  ph  /\  ch )  <->  ( ph  /\  ch  /\  ps ) )
31, 2bitri 242 1  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ph  /\  ch  /\ 
ps ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    /\ w3a 937
This theorem is referenced by:  3simpb  956  elioore  10948  leexp2  11436  pcgcd  13253  xmetrtri  18387  phtpcer  19022  ishl2  19326  ablo32  21876  ablodivdiv  21880  ablodiv32  21882  nvsubsub23  22145  btwncom  25950  btwnswapid2  25954  btwnouttr  25960  cgr3permute1  25984  colinearperm1  25998  endofsegid  26021  colinbtwnle  26054  broutsideof2  26058  outsideofcom  26064  neificl  26461  swrd0swrd  28219  swrdswrd  28221  frgra3v  28454  uunTT1p1  28968  uun123  28982  bnj268  29135  bnj945  29206  bnj944  29371  bnj969  29379  lhpexle2  30869
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator