Theorem 3coml 1234

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

Syntax hints:   -> wi 4   /\ w3a 1002

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 1004

This theorem is referenced by:  3comr  1235  nndir  6653  f1oen2g  6923  f1dom2g  6924  ordiso  7226  addassnqg  7592  ltbtwnnqq  7625  nnanq0  7668  ltasrg  7980  recexgt0sr  7983  axmulass  8083  adddir  8160  axltadd  8239  ltleletr  8251  letr  8252  pnpcan2  8409  subdir  8555  div13ap  8863  zdiv  9558  xrletr  10033  fzen  10268  fzrevral2  10331  fzshftral  10333  fzind2  10475  mulbinom2  10908  ccatlcan  11289  elicc4abs  11645  dvdsnegb  12359  muldvds1  12367  muldvds2  12368  dvdscmul  12369  dvdsmulc  12370  dvdsgcd  12573  mulgcdr  12579  lcmgcdeq  12645  congr  12662  mulgnnass  13734  mettri  15087  cnmet  15244  addcncntoplem  15275