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  6723  f1oen2g  6994  f1dom2g  6995  ordiso  7327  addassnqg  7697  ltbtwnnqq  7730  nnanq0  7773  ltasrg  8085  recexgt0sr  8088  axmulass  8188  adddir  8265  axltadd  8343  ltleletr  8355  letr  8356  pnpcan2  8513  subdir  8659  div13ap  8967  zdiv  9666  xrletr  10141  fzen  10377  fzrevral2  10440  fzshftral  10442  fzind2  10585  mulbinom2  11018  ccatlcan  11410  elicc4abs  11779  dvdsnegb  12494  muldvds1  12502  muldvds2  12503  dvdscmul  12504  dvdsmulc  12505  dvdsgcd  12708  mulgcdr  12714  lcmgcdeq  12780  congr  12797  mulgnnass  13874  mettri  15238  cnmet  15395  addcncntoplem  15426