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  6557  f1oen2g  6823  f1dom2g  6824  ordiso  7111  addassnqg  7466  ltbtwnnqq  7499  nnanq0  7542  ltasrg  7854  recexgt0sr  7857  axmulass  7957  adddir  8034  axltadd  8113  ltleletr  8125  letr  8126  pnpcan2  8283  subdir  8429  div13ap  8737  zdiv  9431  xrletr  9900  fzen  10135  fzrevral2  10198  fzshftral  10200  fzind2  10332  mulbinom2  10765  elicc4abs  11276  dvdsnegb  11990  muldvds1  11998  muldvds2  11999  dvdscmul  12000  dvdsmulc  12001  dvdsgcd  12204  mulgcdr  12210  lcmgcdeq  12276  congr  12293  mulgnnass  13363  mettri  14693  cnmet  14850  addcncntoplem  14881