Theorem 3coml 1212

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

Syntax hints:   -> wi 4   /\ w3a 980

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 982

This theorem is referenced by:  3comr  1213  nndir  6543  f1oen2g  6809  f1dom2g  6810  ordiso  7095  addassnqg  7442  ltbtwnnqq  7475  nnanq0  7518  ltasrg  7830  recexgt0sr  7833  axmulass  7933  adddir  8010  axltadd  8089  ltleletr  8101  letr  8102  pnpcan2  8259  subdir  8405  div13ap  8712  zdiv  9405  xrletr  9874  fzen  10109  fzrevral2  10172  fzshftral  10174  fzind2  10306  mulbinom2  10727  elicc4abs  11238  dvdsnegb  11951  muldvds1  11959  muldvds2  11960  dvdscmul  11961  dvdsmulc  11962  dvdsgcd  12149  mulgcdr  12155  lcmgcdeq  12221  congr  12238  mulgnnass  13227  mettri  14541  cnmet  14698  addcncntoplem  14719