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

Theorem 3comr 1195
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 1194 . 2  |-  ( ( ps  /\  ch  /\  ph )  ->  th )
323coml 1194 1  |-  ( ( ch  /\  ph  /\  ps )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 965
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 967
This theorem is referenced by:  oacan  7002  omlimcl  7032  nnacan  7082  en3lplem2  7836  le2tri3i  9519  ltaddsublt  9978  div12  10031  lemul12b  10201  zdivadd  10728  zdivmul  10729  elfz  11458  fzmmmeqm  11507  fzrev  11534  modmulnn  11740  digit2  12012  digit1  12013  faclbnd5  12089  swrdccatin2  12393  absdiflt  12820  absdifle  12821  dvds0lem  13558  dvdsmulc  13575  dvds2add  13579  dvds2sub  13580  dvdstr  13581  pospropd  15319  fmfil  19532  elfm  19535  xmettri2  19930  stdbdmetval  20104  nmf2  20200  brbtwn  23160  colinearalglem3  23169  colinearalg  23171  isvci  23975  nvtri  24073  nmooge0  24182  his7  24507  his2sub2  24510  braadd  25364  bramul  25365  cnlnadjlem2  25487  pjimai  25595  atcvati  25805  mdsymlem5  25826  colineardim1  28107  ftc1anclem6  28491  stoweidlem2  29816  sigarperm  29915  leaddsuble  30193  mulmoddvds  30265  uun123p3  31563  bnj240  31706  bnj1189  32019
  Copyright terms: Public domain W3C validator