Theorem 3coml 1213

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

Syntax hints:   -> wi 4   /\ w3a 981

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 983

This theorem is referenced by:  3comr  1214  nndir  6601  f1oen2g  6871  f1dom2g  6872  ordiso  7166  addassnqg  7532  ltbtwnnqq  7565  nnanq0  7608  ltasrg  7920  recexgt0sr  7923  axmulass  8023  adddir  8100  axltadd  8179  ltleletr  8191  letr  8192  pnpcan2  8349  subdir  8495  div13ap  8803  zdiv  9498  xrletr  9967  fzen  10202  fzrevral2  10265  fzshftral  10267  fzind2  10407  mulbinom2  10840  ccatlcan  11211  elicc4abs  11566  dvdsnegb  12280  muldvds1  12288  muldvds2  12289  dvdscmul  12290  dvdsmulc  12291  dvdsgcd  12494  mulgcdr  12500  lcmgcdeq  12566  congr  12583  mulgnnass  13654  mettri  15006  cnmet  15163  addcncntoplem  15194