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

Theorem 3comr 1211
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 1210 . 2  |-  ( ( ps  /\  ch  /\  ph )  ->  th )
323coml 1210 1  |-  ( ( ch  /\  ph  /\  ps )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 978
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 980
This theorem is referenced by:  nnacan  6507  le2tri3i  8056  ltaddsublt  8518  div12ap  8640  lemul12b  8807  zdivadd  9331  zdivmul  9332  elfz  10001  fzmmmeqm  10044  fzrev  10070  absdiflt  11085  absdifle  11086  dvds0lem  11792  dvdsmulc  11810  dvds2add  11816  dvds2sub  11817  dvdstr  11819  lcmdvds  12062  psmettri2  13495  xmettri2  13528
  Copyright terms: Public domain W3C validator