Theorem 3coml 1241

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

This proof depends on syntax axioms:   -> wi 4   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  3comr  1242  nndir  6768  f1oen2g  7047  f1dom2g  7048  ordiso  7382  addassnqg  7755  ltbtwnnqq  7788  nnanq0  7831  ltasrg  8143  recexgt0sr  8146  axmulass  8246  adddir  8323  axltadd  8401  ltleletr  8413  letr  8414  pnpcan2  8573  subdir  8720  div13ap  9031  zdiv  9744  xrletr  10226  fzen  10463  fzrevral2  10529  fzshftral  10531  fzind2  10674  mulbinom2  11113  ccatlcan  11511  elicc4abs  11882  dvdsnegb  12599  muldvds1  12607  muldvds2  12608  dvdscmul  12609  dvdsmulc  12610  dvdsgcd  12813  mulgcdr  12819  lcmgcdeq  12885  congr  12902  mulgnnass  14018  mettri  15616  cnmet  15773  addcncntoplem  15804  bcmono  16321