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  10702  leexp2  11172  pcgcd  12946  xmetrtri  17935  phtpcer  18509  ishl2  18803  ablo32  20969  ablodivdiv  20973  ablodiv32  20975  nvsubsub23  21236  ballotlem2  23063  btwncom  24709  btwnswapid2  24713  btwnouttr  24719  cgr3permute1  24743  colinearperm1  24757  endofsegid  24780  colinbtwnle  24813  broutsideof2  24817  outsideofcom  24823  neificl  26570  frgra3v  28426  uunTT1p1  28883  uun123  28897  bnj268  29050  bnj945  29121  bnj944  29286  bnj969  29294  lhpexle2  30821
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