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

Theorem 3comr 1190
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 1189 . 2  |-  ( ( ps  /\  ch  /\  ph )  ->  th )
323coml 1189 1  |-  ( ( ch  /\  ph  /\  ps )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 960
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 962
This theorem is referenced by:  oacan  6983  omlimcl  7013  nnacan  7063  en3lplem2  7817  le2tri3i  9500  ltaddsublt  9959  div12  10012  lemul12b  10182  zdivadd  10709  zdivmul  10710  elfz  11439  fzmmmeqm  11488  fzrev  11515  modmulnn  11721  digit2  11993  digit1  11994  faclbnd5  12070  swrdccatin2  12374  absdiflt  12801  absdifle  12802  dvds0lem  13539  dvdsmulc  13556  dvds2add  13560  dvds2sub  13561  dvdstr  13562  pospropd  15300  fmfil  19476  elfm  19479  xmettri2  19874  stdbdmetval  20048  nmf2  20144  brbtwn  23080  colinearalglem3  23089  colinearalg  23091  isvci  23895  nvtri  23993  nmooge0  24102  his7  24427  his2sub2  24430  braadd  25284  bramul  25285  cnlnadjlem2  25407  pjimai  25515  atcvati  25725  mdsymlem5  25746  colineardim1  28021  ftc1anclem6  28397  stoweidlem2  29722  sigarperm  29821  leaddsuble  30099  mulmoddvds  30171  uun123p3  31378  bnj240  31521  bnj1189  31834
  Copyright terms: Public domain W3C validator