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

Theorem 3comr 1204
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 1203 . 2  |-  ( ( ps  /\  ch  /\  ph )  ->  th )
323coml 1203 1  |-  ( ( ch  /\  ph  /\  ps )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 973
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 975
This theorem is referenced by:  oacan  7194  omlimcl  7224  nnacan  7274  en3lplem2  8028  le2tri3i  9710  ltaddsublt  10172  div12  10225  lemul12b  10395  zdivadd  10928  zdivmul  10929  elfz  11674  fzmmmeqm  11713  fzrev  11738  modmulnn  11977  digit2  12263  digit1  12264  faclbnd5  12340  swrdccatin2  12671  absdiflt  13109  absdifle  13110  dvds0lem  13851  dvdsmulc  13868  dvds2add  13872  dvds2sub  13873  dvdstr  13874  mulmoddvds  13899  pospropd  15617  fmfil  20180  elfm  20183  xmettri2  20578  stdbdmetval  20752  nmf2  20848  brbtwn  23878  colinearalglem3  23887  colinearalg  23889  isvci  25151  nvtri  25249  nmooge0  25358  his7  25683  his2sub2  25686  braadd  26540  bramul  26541  cnlnadjlem2  26663  pjimai  26771  atcvati  26981  mdsymlem5  27002  colineardim1  29288  ftc1anclem6  29672  lcmdvds  30814  stoweidlem2  31302  sigarperm  31544  leaddsuble  31788  uun123p3  32688  bnj240  32831  bnj1189  33144
  Copyright terms: Public domain W3C validator