Theorem 3comr 1273

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

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 |- ( ( ph /\ ps /\ ch ) -> th )
2	1	3coml 1272	. 2 |- ( ( ps /\ ch /\ ph ) -> th )
3	2	3coml 1272	1 |- ( ( ch /\ ph /\ ps ) -> th )

Syntax hints:   -> wi 4   /\ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  oacan  7628  omlimcl  7658  nnacan  7708  en3lplem2  8512  le2tri3i  10167  ltaddsublt  10654  div12  10707  lemul12b  10880  zdivadd  11448  zdivmul  11449  elfz  12332  fzmmmeqm  12374  fzrev  12403  modmulnn  12688  digit2  12997  digit1  12998  faclbnd5  13085  swrdccatin2  13487  absdiflt  14057  absdifle  14058  dvds0lem  14992  dvdsmulc  15009  dvds2add  15015  dvds2sub  15016  dvdstr  15018  mulmoddvds  15051  lcmdvds  15321  pospropd  17134  fmfil  21748  elfm  21751  psmettri2  22114  xmettri2  22145  stdbdmetval  22319  nmf2  22397  isclmi0  22898  iscvsi  22929  brbtwn  25779  colinearalglem3  25788  colinearalg  25790  isvciOLD  27435  nvtri  27525  nmooge0  27622  his7  27947  his2sub2  27950  braadd  28804  bramul  28805  cnlnadjlem2  28927  pjimai  29035  atcvati  29245  mdsymlem5  29266  bnj240  30765  bnj1189  31077  colineardim1  32168  ftc1anclem6  33490  uun123p3  39038  stoweidlem2  40219  sigarperm  41049  leaddsuble  41311