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  8567  subdir  8714  div13ap  9025  zdiv  9738  xrletr  10220  fzen  10457  fzrevral2  10523  fzshftral  10525  fzind2  10668  mulbinom2  11106  ccatlcan  11504  elicc4abs  11875  dvdsnegb  12591  muldvds1  12599  muldvds2  12600  dvdscmul  12601  dvdsmulc  12602  dvdsgcd  12805  mulgcdr  12811  lcmgcdeq  12877  congr  12894  mulgnnass  14009  mettri  15523  cnmet  15680  addcncntoplem  15711  bcmono  16202