Theorem 3coml 1210

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

Syntax hints:   -> wi 4   /\ w3a 978

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 980

This theorem is referenced by:  3comr  1211  nndir  6491  f1oen2g  6755  f1dom2g  6756  ordiso  7035  addassnqg  7381  ltbtwnnqq  7414  nnanq0  7457  ltasrg  7769  recexgt0sr  7772  axmulass  7872  adddir  7948  axltadd  8027  ltleletr  8039  letr  8040  pnpcan2  8197  subdir  8343  div13ap  8650  zdiv  9341  xrletr  9808  fzen  10043  fzrevral2  10106  fzshftral  10108  fzind2  10239  mulbinom2  10637  elicc4abs  11103  dvdsnegb  11815  muldvds1  11823  muldvds2  11824  dvdscmul  11825  dvdsmulc  11826  dvdsgcd  12013  mulgcdr  12019  lcmgcdeq  12083  congr  12100  mulgnnass  13018  mettri  13876  cnmet  14033  addcncntoplem  14054