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  6763  f1oen2g  7041  f1dom2g  7042  ordiso  7376  addassnqg  7749  ltbtwnnqq  7782  nnanq0  7825  ltasrg  8137  recexgt0sr  8140  axmulass  8240  adddir  8317  axltadd  8395  ltleletr  8407  letr  8408  pnpcan2  8566  subdir  8713  div13ap  9023  zdiv  9734  xrletr  10210  fzen  10447  fzrevral2  10513  fzshftral  10515  fzind2  10658  mulbinom2  11093  ccatlcan  11490  elicc4abs  11860  dvdsnegb  12575  muldvds1  12583  muldvds2  12584  dvdscmul  12585  dvdsmulc  12586  dvdsgcd  12789  mulgcdr  12795  lcmgcdeq  12861  congr  12878  mulgnnass  13960  mettri  15474  cnmet  15631  addcncntoplem  15662