Theorem 3coml 1241

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 1240	. 2 |- ( ( ph /\ ch /\ ps ) -> th )
3	2	3com13 1239	1 |- ( ( ps /\ ch /\ ph ) -> th )

Syntax hints:   -> wi 4   /\ w3a 1009

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 1011

This theorem is referenced by:  3comr  1242  nndir  6753  f1oen2g  7031  f1dom2g  7032  ordiso  7366  addassnqg  7739  ltbtwnnqq  7772  nnanq0  7815  ltasrg  8127  recexgt0sr  8130  axmulass  8230  adddir  8307  axltadd  8385  ltleletr  8397  letr  8398  pnpcan2  8556  subdir  8703  div13ap  9013  zdiv  9713  xrletr  10189  fzen  10426  fzrevral2  10491  fzshftral  10493  fzind2  10636  mulbinom2  11071  ccatlcan  11468  elicc4abs  11838  dvdsnegb  12553  muldvds1  12561  muldvds2  12562  dvdscmul  12563  dvdsmulc  12564  dvdsgcd  12767  mulgcdr  12773  lcmgcdeq  12839  congr  12856  mulgnnass  13937  mettri  15397  cnmet  15554  addcncntoplem  15585