Theorem 3coml 1234

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

Syntax hints:   -> wi 4   /\ w3a 1002

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 1004

This theorem is referenced by:  3comr  1235  nndir  6636  f1oen2g  6906  f1dom2g  6907  ordiso  7203  addassnqg  7569  ltbtwnnqq  7602  nnanq0  7645  ltasrg  7957  recexgt0sr  7960  axmulass  8060  adddir  8137  axltadd  8216  ltleletr  8228  letr  8229  pnpcan2  8386  subdir  8532  div13ap  8840  zdiv  9535  xrletr  10004  fzen  10239  fzrevral2  10302  fzshftral  10304  fzind2  10445  mulbinom2  10878  ccatlcan  11250  elicc4abs  11605  dvdsnegb  12319  muldvds1  12327  muldvds2  12328  dvdscmul  12329  dvdsmulc  12330  dvdsgcd  12533  mulgcdr  12539  lcmgcdeq  12605  congr  12622  mulgnnass  13694  mettri  15047  cnmet  15204  addcncntoplem  15235