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

Theorem 3ancomb 945
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 943 . 2  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ps  /\  ph  /\ 
ch ) )
2 3anrot 941 . 2  |-  ( ( ps  /\  ph  /\  ch )  <->  ( ph  /\  ch  /\  ps ) )
31, 2bitri 241 1  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ph  /\  ch  /\ 
ps ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    /\ w3a 936
This theorem is referenced by:  3simpb  955  elioore  10902  leexp2  11389  pcgcd  13206  xmetrtri  18338  phtpcer  18973  ishl2  19277  ablo32  21827  ablodivdiv  21831  ablodiv32  21833  nvsubsub23  22096  btwncom  25852  btwnswapid2  25856  btwnouttr  25862  cgr3permute1  25886  colinearperm1  25900  endofsegid  25923  colinbtwnle  25956  broutsideof2  25960  outsideofcom  25966  neificl  26349  swrd0swrd  28009  swrdswrd  28011  frgra3v  28106  uunTT1p1  28615  uun123  28629  bnj268  28779  bnj945  28850  bnj944  29015  bnj969  29023  lhpexle2  30492
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