Theorem 3coml 1212

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

Syntax hints:   -> wi 4   /\ w3a 980

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 982

This theorem is referenced by:  3comr  1213  nndir  6516  f1oen2g  6782  f1dom2g  6783  ordiso  7066  addassnqg  7412  ltbtwnnqq  7445  nnanq0  7488  ltasrg  7800  recexgt0sr  7803  axmulass  7903  adddir  7979  axltadd  8058  ltleletr  8070  letr  8071  pnpcan2  8228  subdir  8374  div13ap  8681  zdiv  9372  xrletr  9840  fzen  10075  fzrevral2  10138  fzshftral  10140  fzind2  10271  mulbinom2  10671  elicc4abs  11138  dvdsnegb  11850  muldvds1  11858  muldvds2  11859  dvdscmul  11860  dvdsmulc  11861  dvdsgcd  12048  mulgcdr  12054  lcmgcdeq  12118  congr  12135  mulgnnass  13114  mettri  14350  cnmet  14507  addcncntoplem  14528