Theorem 3coml 1236

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

Syntax hints:   -> wi 4   /\ w3a 1004

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 1006

This theorem is referenced by:  3comr  1237  nndir  6658  f1oen2g  6928  f1dom2g  6929  ordiso  7235  addassnqg  7602  ltbtwnnqq  7635  nnanq0  7678  ltasrg  7990  recexgt0sr  7993  axmulass  8093  adddir  8170  axltadd  8249  ltleletr  8261  letr  8262  pnpcan2  8419  subdir  8565  div13ap  8873  zdiv  9568  xrletr  10043  fzen  10278  fzrevral2  10341  fzshftral  10343  fzind2  10486  mulbinom2  10919  ccatlcan  11303  elicc4abs  11672  dvdsnegb  12387  muldvds1  12395  muldvds2  12396  dvdscmul  12397  dvdsmulc  12398  dvdsgcd  12601  mulgcdr  12607  lcmgcdeq  12673  congr  12690  mulgnnass  13762  mettri  15116  cnmet  15273  addcncntoplem  15304