Theorem 3coml 1236

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

Syntax hints:   -> wi 4   /\ w3a 1004

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 1006

This theorem is referenced by:  3comr  1237  nndir  6657  f1oen2g  6927  f1dom2g  6928  ordiso  7234  addassnqg  7601  ltbtwnnqq  7634  nnanq0  7677  ltasrg  7989  recexgt0sr  7992  axmulass  8092  adddir  8169  axltadd  8248  ltleletr  8260  letr  8261  pnpcan2  8418  subdir  8564  div13ap  8872  zdiv  9567  xrletr  10042  fzen  10277  fzrevral2  10340  fzshftral  10342  fzind2  10484  mulbinom2  10917  ccatlcan  11298  elicc4abs  11654  dvdsnegb  12368  muldvds1  12376  muldvds2  12377  dvdscmul  12378  dvdsmulc  12379  dvdsgcd  12582  mulgcdr  12588  lcmgcdeq  12654  congr  12671  mulgnnass  13743  mettri  15096  cnmet  15253  addcncntoplem  15284