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

Theorem com3r 73
Description: Commutation of antecedents. Rotate right. (Contributed by NM, 25-Apr-1994.)
Hypothesis
Ref Expression
com3.1  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
Assertion
Ref Expression
com3r  |-  ( ch 
->  ( ph  ->  ( ps  ->  th ) ) )

Proof of Theorem com3r
StepHypRef Expression
1 com3.1 . . 3  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
21com23 72 . 2  |-  ( ph  ->  ( ch  ->  ( ps  ->  th ) ) )
32com12 27 1  |-  ( ch 
->  ( ph  ->  ( ps  ->  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7
This theorem is referenced by:  com13  74  com3l  75  com14  82  expd  245  moexexdc  1984  euexex  1985  mob  2723  issref  4707  relresfld  4847  poxp  5853  nndi  6065  nnmass  6066  distrlem5prl  6684  distrlem5pru  6685  flqeqceilz  9160  ialgcvga  9890  ialgfx  9891
  Copyright terms: Public domain W3C validator