Theorem 3coml 1189

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

Syntax hints:   -> wi 4   /\ w3a 963

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

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

This theorem is referenced by:  3comr  1190  nndir  6426  f1oen2g  6689  f1dom2g  6690  ordiso  6966  addassnqg  7281  ltbtwnnqq  7314  nnanq0  7357  ltasrg  7669  recexgt0sr  7672  axmulass  7772  adddir  7848  axltadd  7926  ltleletr  7938  letr  7939  pnpcan2  8094  subdir  8240  div13ap  8545  zdiv  9231  xrletr  9690  fzen  9923  fzrevral2  9986  fzshftral  9988  fzind2  10116  mulbinom2  10512  elicc4abs  10971  dvdsnegb  11677  muldvds1  11685  muldvds2  11686  dvdscmul  11687  dvdsmulc  11688  dvdsgcd  11867  mulgcdr  11873  lcmgcdeq  11931  congr  11948  mettri  12712  cnmet  12869  addcncntoplem  12890