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  6548  f1oen2g  6814  f1dom2g  6815  ordiso  7102  addassnqg  7449  ltbtwnnqq  7482  nnanq0  7525  ltasrg  7837  recexgt0sr  7840  axmulass  7940  adddir  8017  axltadd  8096  ltleletr  8108  letr  8109  pnpcan2  8266  subdir  8412  div13ap  8720  zdiv  9414  xrletr  9883  fzen  10118  fzrevral2  10181  fzshftral  10183  fzind2  10315  mulbinom2  10748  elicc4abs  11259  dvdsnegb  11973  muldvds1  11981  muldvds2  11982  dvdscmul  11983  dvdsmulc  11984  dvdsgcd  12179  mulgcdr  12185  lcmgcdeq  12251  congr  12268  mulgnnass  13287  mettri  14609  cnmet  14766  addcncntoplem  14797