Theorem 3coml 1200

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

Syntax hints:   -> wi 4   /\ w3a 968

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 970

This theorem is referenced by:  3comr  1201  nndir  6458  f1oen2g  6721  f1dom2g  6722  ordiso  7001  addassnqg  7323  ltbtwnnqq  7356  nnanq0  7399  ltasrg  7711  recexgt0sr  7714  axmulass  7814  adddir  7890  axltadd  7968  ltleletr  7980  letr  7981  pnpcan2  8138  subdir  8284  div13ap  8589  zdiv  9279  xrletr  9744  fzen  9978  fzrevral2  10041  fzshftral  10043  fzind2  10174  mulbinom2  10571  elicc4abs  11036  dvdsnegb  11748  muldvds1  11756  muldvds2  11757  dvdscmul  11758  dvdsmulc  11759  dvdsgcd  11945  mulgcdr  11951  lcmgcdeq  12015  congr  12032  mettri  13013  cnmet  13170  addcncntoplem  13191