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

Theorem 3comr 1151
Description: Commutation in antecedent. Rotate right. (Contributed by NM, 28-Jan-1996.)
Hypothesis
Ref Expression
3exp.1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Assertion
Ref Expression
3comr  |-  ( ( ch  /\  ph  /\  ps )  ->  th )

Proof of Theorem 3comr
StepHypRef Expression
1 3exp.1 . . 3  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
213coml 1150 . 2  |-  ( ( ps  /\  ch  /\  ph )  ->  th )
323coml 1150 1  |-  ( ( ch  /\  ph  /\  ps )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 924
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 926
This theorem is referenced by:  nnacan  6271  le2tri3i  7593  ltaddsublt  8048  div12ap  8161  lemul12b  8322  zdivadd  8835  zdivmul  8836  elfz  9430  fzmmmeqm  9472  fzrev  9498  absdiflt  10525  absdifle  10526  dvds0lem  11084  dvdsmulc  11102  dvds2add  11108  dvds2sub  11109  dvdstr  11111  lcmdvds  11339
  Copyright terms: Public domain W3C validator