Theorem 3coml 1212

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

Syntax hints:   -> wi 4   /\ w3a 980

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 982

This theorem is referenced by:  3comr  1213  nndir  6575  f1oen2g  6845  f1dom2g  6846  ordiso  7137  addassnqg  7494  ltbtwnnqq  7527  nnanq0  7570  ltasrg  7882  recexgt0sr  7885  axmulass  7985  adddir  8062  axltadd  8141  ltleletr  8153  letr  8154  pnpcan2  8311  subdir  8457  div13ap  8765  zdiv  9460  xrletr  9929  fzen  10164  fzrevral2  10227  fzshftral  10229  fzind2  10366  mulbinom2  10799  elicc4abs  11376  dvdsnegb  12090  muldvds1  12098  muldvds2  12099  dvdscmul  12100  dvdsmulc  12101  dvdsgcd  12304  mulgcdr  12310  lcmgcdeq  12376  congr  12393  mulgnnass  13464  mettri  14816  cnmet  14973  addcncntoplem  15004