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

Theorem com3r 77
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 76 . 2  |-  ( ph  ->  ( ch  ->  ( ps  ->  th ) ) )
32com12 30 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  78  com3l  79  com14  86  expd  249  moexexdc  2000  euexex  2001  mob  2746  issref  4735  relresfld  4875  poxp  5881  nndi  6096  nnmass  6097  distrlem5prl  6742  distrlem5pru  6743  flqeqceilz  9268  divconjdvds  10161  ialgcvga  10273  ialgfx  10274
  Copyright terms: Public domain W3C validator