Theorem 3coml 1171

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

Syntax hints:   -> wi 4   /\ w3a 945

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

This theorem depends on definitions:  df-bi 116  df-3an 947

This theorem is referenced by:  3comr  1172  nndir  6340  f1oen2g  6603  f1dom2g  6604  ordiso  6873  addassnqg  7138  ltbtwnnqq  7171  nnanq0  7214  ltasrg  7513  recexgt0sr  7516  axmulass  7608  adddir  7681  axltadd  7758  ltleletr  7769  letr  7770  pnpcan2  7925  subdir  8067  div13ap  8366  zdiv  9043  xrletr  9484  fzen  9716  fzrevral2  9779  fzshftral  9781  fzind2  9909  mulbinom2  10301  elicc4abs  10758  dvdsnegb  11358  muldvds1  11366  muldvds2  11367  dvdscmul  11368  dvdsmulc  11369  dvdsgcd  11546  mulgcdr  11552  lcmgcdeq  11610  congr  11627  mettri  12362  cnmet  12519  addcncntoplem  12537