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

Theorem 3ancomb 943
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 941 . 2  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ps  /\  ph  /\ 
ch ) )
2 3anrot 939 . 2  |-  ( ( ps  /\  ph  /\  ch )  <->  ( ph  /\  ch  /\  ps ) )
31, 2bitri 240 1  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ph  /\  ch  /\ 
ps ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ w3a 934
This theorem is referenced by:  3simpb  953  elioore  10686  leexp2  11156  pcgcd  12930  xmetrtri  17919  phtpcer  18493  ishl2  18787  ablo32  20953  ablodivdiv  20957  ablodiv32  20959  nvsubsub23  21220  ballotlem2  23047  btwncom  24637  btwnswapid2  24641  btwnouttr  24647  cgr3permute1  24671  colinearperm1  24685  endofsegid  24708  colinbtwnle  24741  broutsideof2  24745  outsideofcom  24751  neificl  26467  frgra3v  28180  uunTT1p1  28569  uun123  28583  bnj268  28734  bnj945  28805  bnj944  28970  bnj969  28978  lhpexle2  30199
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