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  6644  f1oen2g  6914  f1dom2g  6915  ordiso  7214  addassnqg  7580  ltbtwnnqq  7613  nnanq0  7656  ltasrg  7968  recexgt0sr  7971  axmulass  8071  adddir  8148  axltadd  8227  ltleletr  8239  letr  8240  pnpcan2  8397  subdir  8543  div13ap  8851  zdiv  9546  xrletr  10016  fzen  10251  fzrevral2  10314  fzshftral  10316  fzind2  10457  mulbinom2  10890  ccatlcan  11266  elicc4abs  11621  dvdsnegb  12335  muldvds1  12343  muldvds2  12344  dvdscmul  12345  dvdsmulc  12346  dvdsgcd  12549  mulgcdr  12555  lcmgcdeq  12621  congr  12638  mulgnnass  13710  mettri  15063  cnmet  15220  addcncntoplem  15251