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

Theorem 3comr 1202
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 1201 . 2  |-  ( ( ps  /\  ch  /\  ph )  ->  th )
323coml 1201 1  |-  ( ( ch  /\  ph  /\  ps )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 971
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 369  df-3an 973
This theorem is referenced by:  oacan  7189  omlimcl  7219  nnacan  7269  en3lplem2  8023  le2tri3i  9703  ltaddsublt  10172  div12  10225  lemul12b  10395  zdivadd  10930  zdivmul  10931  elfz  11681  fzmmmeqm  11721  fzrev  11746  modmulnn  11995  digit2  12281  digit1  12282  faclbnd5  12358  swrdccatin2  12703  absdiflt  13232  absdifle  13233  dvds0lem  14078  dvdsmulc  14095  dvds2add  14099  dvds2sub  14100  dvdstr  14102  mulmoddvds  14128  pospropd  15963  fmfil  20611  elfm  20614  psmettri2  20979  xmettri2  21009  stdbdmetval  21183  nmf2  21279  brbtwn  24404  colinearalglem3  24413  colinearalg  24415  isvci  25673  nvtri  25771  nmooge0  25880  his7  26205  his2sub2  26208  braadd  27062  bramul  27063  cnlnadjlem2  27185  pjimai  27293  atcvati  27503  mdsymlem5  27524  colineardim1  29939  ftc1anclem6  30335  lcmdvds  31455  stoweidlem2  32023  sigarperm  32316  leaddsuble  32693  uun123p3  34002  bnj240  34152  bnj1189  34466
  Copyright terms: Public domain W3C validator