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  6576  f1oen2g  6846  f1dom2g  6847  ordiso  7138  addassnqg  7495  ltbtwnnqq  7528  nnanq0  7571  ltasrg  7883  recexgt0sr  7886  axmulass  7986  adddir  8063  axltadd  8142  ltleletr  8154  letr  8155  pnpcan2  8312  subdir  8458  div13ap  8766  zdiv  9461  xrletr  9930  fzen  10165  fzrevral2  10228  fzshftral  10230  fzind2  10368  mulbinom2  10801  elicc4abs  11405  dvdsnegb  12119  muldvds1  12127  muldvds2  12128  dvdscmul  12129  dvdsmulc  12130  dvdsgcd  12333  mulgcdr  12339  lcmgcdeq  12405  congr  12422  mulgnnass  13493  mettri  14845  cnmet  15002  addcncntoplem  15033