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

Theorem 3comr 1172
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 1171 . 2  |-  ( ( ps  /\  ch  /\  ph )  ->  th )
323coml 1171 1  |-  ( ( ch  /\  ph  /\  ps )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 945
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 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:  nnacan  6374  le2tri3i  7836  ltaddsublt  8296  div12ap  8417  lemul12b  8579  zdivadd  9094  zdivmul  9095  elfz  9747  fzmmmeqm  9789  fzrev  9815  absdiflt  10815  absdifle  10816  dvds0lem  11410  dvdsmulc  11428  dvds2add  11434  dvds2sub  11435  dvdstr  11437  lcmdvds  11667  psmettri2  12403  xmettri2  12436
  Copyright terms: Public domain W3C validator