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

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
StepHypRef Expression
1 3exp.1 . . 3  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
213com23 1211 . 2  |-  ( (
ph  /\  ch  /\  ps )  ->  th )
323com13 1210 1  |-  ( ( ps  /\  ch  /\  ph )  ->  th )
Colors of variables: wff set class
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  6516  f1oen2g  6782  f1dom2g  6783  ordiso  7066  addassnqg  7412  ltbtwnnqq  7445  nnanq0  7488  ltasrg  7800  recexgt0sr  7803  axmulass  7903  adddir  7979  axltadd  8058  ltleletr  8070  letr  8071  pnpcan2  8228  subdir  8374  div13ap  8681  zdiv  9372  xrletr  9840  fzen  10075  fzrevral2  10138  fzshftral  10140  fzind2  10271  mulbinom2  10671  elicc4abs  11138  dvdsnegb  11850  muldvds1  11858  muldvds2  11859  dvdscmul  11860  dvdsmulc  11861  dvdsgcd  12048  mulgcdr  12054  lcmgcdeq  12118  congr  12135  mulgnnass  13114  mettri  14350  cnmet  14507  addcncntoplem  14528
  Copyright terms: Public domain W3C validator