Theorem 3coml 1188

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

Syntax hints:   -> wi 4   /\ w3a 962

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 964

This theorem is referenced by:  3comr  1189  nndir  6386  f1oen2g  6649  f1dom2g  6650  ordiso  6921  addassnqg  7190  ltbtwnnqq  7223  nnanq0  7266  ltasrg  7578  recexgt0sr  7581  axmulass  7681  adddir  7757  axltadd  7834  ltleletr  7846  letr  7847  pnpcan2  8002  subdir  8148  div13ap  8453  zdiv  9139  xrletr  9591  fzen  9823  fzrevral2  9886  fzshftral  9888  fzind2  10016  mulbinom2  10408  elicc4abs  10866  dvdsnegb  11510  muldvds1  11518  muldvds2  11519  dvdscmul  11520  dvdsmulc  11521  dvdsgcd  11700  mulgcdr  11706  lcmgcdeq  11764  congr  11781  mettri  12542  cnmet  12699  addcncntoplem  12720