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

Theorem 3ancomb 974
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 972 . 2  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ps  /\  ph  /\ 
ch ) )
2 3anrot 970 . 2  |-  ( ( ps  /\  ph  /\  ch )  <->  ( ph  /\  ch  /\  ps ) )
31, 2bitri 249 1  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ph  /\  ch  /\ 
ps ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ 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:  3simpb  986  an33rean  1333  elioore  11445  leexp2  12039  swrdswrd  12476  pcgcd  14066  xmetrtri  20072  phtpcer  20709  ishl2  21024  ablo32  23952  ablodivdiv  23956  ablodiv32  23958  nvsubsub23  24221  btwncom  28212  btwnswapid2  28216  btwnouttr  28222  cgr3permute1  28246  colinearperm1  28260  endofsegid  28283  colinbtwnle  28316  broutsideof2  28320  outsideofcom  28326  neificl  28820  frgra3v  30765  numclwwlkovf2num  30849  alsi-no-surprise  31503  uunTT1p1  31882  uun123  31896  bnj268  32052  bnj945  32122  bnj944  32286  bnj969  32294  lhpexle2  34017
  Copyright terms: Public domain W3C validator