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  6767  f1oen2g  7045  f1dom2g  7046  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  9745  xrletr  10227  fzen  10464  fzrevral2  10530  fzshftral  10532  fzind2  10675  mulbinom2  11114  ccatlcan  11512  elicc4abs  11883  dvdsnegb  12600  muldvds1  12608  muldvds2  12609  dvdscmul  12610  dvdsmulc  12611  dvdsgcd  12814  mulgcdr  12820  lcmgcdeq  12886  congr  12903  mulgnnass  14019  mettri  15599  cnmet  15756  addcncntoplem  15787  bcmono  16304