Theorem 3coml 1237

Description: Commutation in antecedent. Rotate left. (Contributed by NM, 28-Jan-1996.)

Hypothesis

Ref	Expression
3exp.1	|- ( ( ph /\ ps /\ ch ) -> th )

Assertion

Ref	Expression
3coml	|- ( ( ps /\ ch /\ ph ) -> th )

Proof of Theorem 3coml

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 |- ( ( ph /\ ps /\ ch ) -> th )
2	1	3com23 1236	. 2 |- ( ( ph /\ ch /\ ps ) -> th )
3	2	3com13 1235	1 |- ( ( ps /\ ch /\ ph ) -> th )

Syntax hints:   -> wi 4   /\ w3a 1005

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 1007

This theorem is referenced by:  3comr  1238  nndir  6738  f1oen2g  7009  f1dom2g  7010  ordiso  7342  addassnqg  7715  ltbtwnnqq  7748  nnanq0  7791  ltasrg  8103  recexgt0sr  8106  axmulass  8206  adddir  8283  axltadd  8361  ltleletr  8373  letr  8374  pnpcan2  8532  subdir  8679  div13ap  8989  zdiv  9689  xrletr  10165  fzen  10402  fzrevral2  10467  fzshftral  10469  fzind2  10612  mulbinom2  11047  ccatlcan  11440  elicc4abs  11810  dvdsnegb  12525  muldvds1  12533  muldvds2  12534  dvdscmul  12535  dvdsmulc  12536  dvdsgcd  12739  mulgcdr  12745  lcmgcdeq  12811  congr  12828  mulgnnass  13916  mettri  15370  cnmet  15527  addcncntoplem  15558