Theorem 3coml 1111

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

Syntax hints:   -> wi 4   /\ w3a 885

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110  df-3an 887

This theorem is referenced by:  3comr  1112  nndir  6069  f1oen2g  6235  f1dom2g  6236  ordiso  6358  addassnqg  6480  ltbtwnnqq  6513  nnanq0  6556  ltasrg  6855  recexgt0sr  6858  axmulass  6947  adddir  7018  axltadd  7089  ltleletr  7100  letr  7101  pnpcan2  7251  subdir  7383  div13ap  7672  zdiv  8328  xrletr  8724  fzen  8907  fzrevral2  8968  fzshftral  8970  fzind2  9095  elicc4abs  9690