Theorem 3coml 1205

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

Syntax hints:   -> wi 4   /\ w3a 973

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 975

This theorem is referenced by:  3comr  1206  nndir  6469  f1oen2g  6733  f1dom2g  6734  ordiso  7013  addassnqg  7344  ltbtwnnqq  7377  nnanq0  7420  ltasrg  7732  recexgt0sr  7735  axmulass  7835  adddir  7911  axltadd  7989  ltleletr  8001  letr  8002  pnpcan2  8159  subdir  8305  div13ap  8610  zdiv  9300  xrletr  9765  fzen  9999  fzrevral2  10062  fzshftral  10064  fzind2  10195  mulbinom2  10592  elicc4abs  11058  dvdsnegb  11770  muldvds1  11778  muldvds2  11779  dvdscmul  11780  dvdsmulc  11781  dvdsgcd  11967  mulgcdr  11973  lcmgcdeq  12037  congr  12054  mettri  13167  cnmet  13324  addcncntoplem  13345