ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  3coml Unicode version

Theorem 3coml 1146
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
StepHypRef Expression
1 3exp.1 . . 3  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
213com23 1145 . 2  |-  ( (
ph  /\  ch  /\  ps )  ->  th )
323com13 1144 1  |-  ( ( ps  /\  ch  /\  ph )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 920
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115  df-3an 922
This theorem is referenced by:  3comr  1147  nndir  6127  f1oen2g  6294  f1dom2g  6295  ordiso  6496  addassnqg  6623  ltbtwnnqq  6656  nnanq0  6699  ltasrg  6998  recexgt0sr  7001  axmulass  7090  adddir  7161  axltadd  7238  ltleletr  7249  letr  7250  pnpcan2  7404  subdir  7546  div13ap  7837  zdiv  8505  xrletr  8943  fzen  9127  fzrevral2  9188  fzshftral  9190  fzind2  9314  mulbinom2  9675  elicc4abs  10107  dvdsnegb  10346  muldvds1  10354  muldvds2  10355  dvdscmul  10356  dvdsmulc  10357  dvdsgcd  10534  mulgcdr  10540  lcmgcdeq  10598  congr  10615
  Copyright terms: Public domain W3C validator