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

Theorem 3coml 1171
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 1170 . 2  |-  ( (
ph  /\  ch  /\  ps )  ->  th )
323com13 1169 1  |-  ( ( ps  /\  ch  /\  ph )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 945
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 947
This theorem is referenced by:  3comr  1172  nndir  6340  f1oen2g  6603  f1dom2g  6604  ordiso  6873  addassnqg  7138  ltbtwnnqq  7171  nnanq0  7214  ltasrg  7513  recexgt0sr  7516  axmulass  7608  adddir  7681  axltadd  7758  ltleletr  7769  letr  7770  pnpcan2  7925  subdir  8067  div13ap  8366  zdiv  9043  xrletr  9484  fzen  9716  fzrevral2  9779  fzshftral  9781  fzind2  9909  mulbinom2  10301  elicc4abs  10758  dvdsnegb  11358  muldvds1  11366  muldvds2  11367  dvdscmul  11368  dvdsmulc  11369  dvdsgcd  11546  mulgcdr  11552  lcmgcdeq  11610  congr  11627  mettri  12362  cnmet  12519  addcncntoplem  12537
  Copyright terms: Public domain W3C validator