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

Theorem 3comr 1147
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 1146 . 2  |-  ( ( ps  /\  ch  /\  ph )  ->  th )
323coml 1146 1  |-  ( ( ch  /\  ph  /\  ps )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 920
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 922
This theorem is referenced by:  nnacan  6172  le2tri3i  7338  ltaddsublt  7790  div12ap  7901  lemul12b  8058  zdivadd  8569  zdivmul  8570  elfz  9163  fzmmmeqm  9204  fzrev  9229  absdiflt  10179  absdifle  10180  dvds0lem  10413  dvdsmulc  10431  dvds2add  10437  dvds2sub  10438  dvdstr  10440  lcmdvds  10668
  Copyright terms: Public domain W3C validator