Theorem 3coml 1213

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

Syntax hints:   -> wi 4   /\ w3a 981

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 983

This theorem is referenced by:  3comr  1214  nndir  6599  f1oen2g  6869  f1dom2g  6870  ordiso  7164  addassnqg  7530  ltbtwnnqq  7563  nnanq0  7606  ltasrg  7918  recexgt0sr  7921  axmulass  8021  adddir  8098  axltadd  8177  ltleletr  8189  letr  8190  pnpcan2  8347  subdir  8493  div13ap  8801  zdiv  9496  xrletr  9965  fzen  10200  fzrevral2  10263  fzshftral  10265  fzind2  10405  mulbinom2  10838  ccatlcan  11209  elicc4abs  11520  dvdsnegb  12234  muldvds1  12242  muldvds2  12243  dvdscmul  12244  dvdsmulc  12245  dvdsgcd  12448  mulgcdr  12454  lcmgcdeq  12520  congr  12537  mulgnnass  13608  mettri  14960  cnmet  15117  addcncntoplem  15148