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

Theorem 3ancomb 967
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 965 . 2  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ps  /\  ph  /\ 
ch ) )
2 3anrot 963 . 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 958
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 960
This theorem is referenced by:  3simpb  979  an33rean  1325  elioore  11318  leexp2  11902  swrdswrd  12338  pcgcd  13927  xmetrtri  19772  phtpcer  20409  ishl2  20724  ablo32  23596  ablodivdiv  23600  ablodiv32  23602  nvsubsub23  23865  btwncom  27892  btwnswapid2  27896  btwnouttr  27902  cgr3permute1  27926  colinearperm1  27940  endofsegid  27963  colinbtwnle  27996  broutsideof2  28000  outsideofcom  28006  neificl  28493  frgra3v  30440  numclwwlkovf2num  30524  alsi-no-surprise  30876  uunTT1p1  31250  uun123  31264  bnj268  31420  bnj945  31490  bnj944  31654  bnj969  31662  lhpexle2  33248
  Copyright terms: Public domain W3C validator