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

Theorem 3comr 1159
Description: Commutation in antecedent. Rotate right. (Contributed by NM, 28-Jan-1996.)
Hypothesis
Ref Expression
3exp.1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Assertion
Ref Expression
3comr  |-  ( ( ch  /\  ph  /\  ps )  ->  th )

Proof of Theorem 3comr
StepHypRef Expression
1 3exp.1 . . 3  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
213coml 1158 . 2  |-  ( ( ps  /\  ch  /\  ph )  ->  th )
323coml 1158 1  |-  ( ( ch  /\  ph  /\  ps )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 934
This theorem is referenced by:  oacan  6562  omlimcl  6592  nnacan  6642  en3lplem2  7433  le2tri3i  8965  div12  9462  lemul12b  9629  zdivadd  10099  zdivmul  10100  elfz  10804  fzrev  10862  modmulnn  11004  digit2  11250  digit1  11251  faclbnd5  11327  absdiflt  11817  absdifle  11818  dvds0lem  12555  dvdsmulc  12572  dvds2add  12576  dvds2sub  12577  dvdstr  12578  pospropd  14254  fmfil  17655  elfm  17658  xmettri2  17921  stdbdmetval  18076  nmf2  18131  isvci  21154  nvtri  21252  nmooge0  21361  his7  21685  his2sub2  21688  braadd  22541  bramul  22542  cnlnadjlem2  22664  pjimai  22772  atcvati  22982  mdsymlem5  23003  brbtwn  24599  colinearalglem3  24608  colinearalg  24610  colineardim1  24756  sigarperm  27953  uun123p3  28900  bnj240  29040  bnj1189  29355
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