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

Theorem 3anrot 977
Description: Rotation law for triple conjunction. (Contributed by NM, 8-Apr-1994.)
Assertion
Ref Expression
3anrot  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ps  /\  ch  /\ 
ph ) )

Proof of Theorem 3anrot
StepHypRef Expression
1 ancom 450 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  <->  ( ( ps  /\  ch )  /\  ph ) )
2 3anass 976 . 2  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ph  /\  ( ps  /\  ch ) ) )
3 df-3an 974 . 2  |-  ( ( ps  /\  ch  /\  ph )  <->  ( ( ps 
/\  ch )  /\  ph ) )
41, 2, 33bitr4i 277 1  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ps  /\  ch  /\ 
ph ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 369    /\ w3a 972
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 974
This theorem is referenced by:  3ancomb  981  3anrev  983  3simpc  994  wefrc  4860  ordelord  4887  f13dfv  6162  fr3nr  6597  omword  7218  nnmcan  7282  pmtr3ncomlem1  16369  srgrmhm  17058  isphld  18559  ordtbaslem  19559  xmetpsmet  20721  comet  20886  cphassr  21528  srabn  21670  lgsdi  23476  colinearalglem2  24079  nb3grapr  24322  nb3grapr2  24323  nb3gra2nb  24324  cusgra3v  24333  frgra3v  24871  dipassr  25630  brapply  29560  brrestrict  29571  dfrdg4  29572  cgrid2  29625  cgr3permute3  29669  cgr3permute2  29671  cgr3permute4  29672  cgr3permute5  29673  colinearperm1  29684  colinearperm3  29685  colinearperm2  29686  colinearperm4  29687  colinearperm5  29688  colinearxfr  29697  endofsegid  29707  colinbtwnle  29740  broutsideof2  29744  dmncan2  30446  lincvalpr  32749  alimp-no-surprise  32926  uunTT1p2  33320  uunT11p1  33322  uunT12p2  33326  uunT12p4  33328  3anidm12p2  33332  uun2221p1  33339  en3lplem2VD  33372  bnj170  33478  bnj290  33490  bnj545  33681  bnj571  33692  bnj594  33698  isltrn2N  35567
  Copyright terms: Public domain W3C validator