Theorem 3coml 1210

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

Syntax hints:   -> wi 4   /\ w3a 978

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 980

This theorem is referenced by:  3comr  1211  nndir  6486  f1oen2g  6750  f1dom2g  6751  ordiso  7030  addassnqg  7376  ltbtwnnqq  7409  nnanq0  7452  ltasrg  7764  recexgt0sr  7767  axmulass  7867  adddir  7943  axltadd  8021  ltleletr  8033  letr  8034  pnpcan2  8191  subdir  8337  div13ap  8644  zdiv  9335  xrletr  9802  fzen  10036  fzrevral2  10099  fzshftral  10101  fzind2  10232  mulbinom2  10629  elicc4abs  11094  dvdsnegb  11806  muldvds1  11814  muldvds2  11815  dvdscmul  11816  dvdsmulc  11817  dvdsgcd  12003  mulgcdr  12009  lcmgcdeq  12073  congr  12090  mulgnnass  12945  mettri  13655  cnmet  13812  addcncntoplem  13833