Theorem 3coml 1241

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

This proof depends on syntax axioms:   -> wi 4   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  3comr  1242  nndir  6763  f1oen2g  7041  f1dom2g  7042  ordiso  7377  addassnqg  7750  ltbtwnnqq  7783  nnanq0  7826  ltasrg  8138  recexgt0sr  8141  axmulass  8241  adddir  8318  axltadd  8396  ltleletr  8408  letr  8409  pnpcan2  8568  subdir  8715  div13ap  9026  zdiv  9739  xrletr  10221  fzen  10458  fzrevral2  10524  fzshftral  10526  fzind2  10669  mulbinom2  11108  ccatlcan  11506  elicc4abs  11877  dvdsnegb  12594  muldvds1  12602  muldvds2  12603  dvdscmul  12604  dvdsmulc  12605  dvdsgcd  12808  mulgcdr  12814  lcmgcdeq  12880  congr  12897  mulgnnass  14013  mettri  15565  cnmet  15722  addcncntoplem  15753  bcmono  16265