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

Theorem 3ancomb 982
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 980 . 2  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ps  /\  ph  /\ 
ch ) )
2 3anrot 978 . 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 973
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 975
This theorem is referenced by:  3simpb  994  an33rean  1342  elioore  11571  leexp2  12200  swrdswrd  12665  pcgcd  14277  xmetrtri  20726  phtpcer  21363  ishl2  21678  frgra3v  24825  numclwwlkovf2num  24909  ablo32  25111  ablodivdiv  25115  ablodiv32  25117  nvsubsub23  25380  btwncom  29591  btwnswapid2  29595  btwnouttr  29601  cgr3permute1  29625  colinearperm1  29639  endofsegid  29662  colinbtwnle  29695  broutsideof2  29699  outsideofcom  29705  neificl  30173  alsi-no-surprise  32693  uunTT1p1  33072  uun123  33086  bnj268  33242  bnj945  33312  bnj944  33476  bnj969  33484  lhpexle2  35207
  Copyright terms: Public domain W3C validator