(A ^ B) -&gt; C 
|------------------ 
|  | A 
|  |--------------- 
|  |  | B 
|  |  |------------ 
|  |  | A ^ B 
|  |  | C 
|  | B -&gt; C 
| A -&gt; (B -&gt; C)

"The same proof in Peirce's Existential Graphs":

( A B ( C ))   [&lt;=&gt;]   ( A ( ( B ( C )) ))

¤~~~~~~~~~¤~~~~~~~~~¤~NOITATIC~¤~~~~~~~~~¤~~~~~~~~~¤

In RefLog syntax for Peirce's Alpha, this looks like so:

|                               B   C
|                               o---o
|      AB   C               A   |
|       o---o       