Theorem 3coml 1146

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

Syntax hints:   -> wi 4   /\ w3a 920

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

This theorem depends on definitions:  df-bi 115  df-3an 922

This theorem is referenced by:  3comr  1147  nndir  6127  f1oen2g  6294  f1dom2g  6295  ordiso  6496  addassnqg  6623  ltbtwnnqq  6656  nnanq0  6699  ltasrg  6998  recexgt0sr  7001  axmulass  7090  adddir  7161  axltadd  7238  ltleletr  7249  letr  7250  pnpcan2  7404  subdir  7546  div13ap  7837  zdiv  8505  xrletr  8943  fzen  9127  fzrevral2  9188  fzshftral  9190  fzind2  9314  mulbinom2  9675  elicc4abs  10107  dvdsnegb  10346  muldvds1  10354  muldvds2  10355  dvdscmul  10356  dvdsmulc  10357  dvdsgcd  10534  mulgcdr  10540  lcmgcdeq  10598  congr  10615