| r                 hyp
|-
| rvs               1 dis_int
| | p&q             hyp
| |-
| | p               3 conj_elim
| | pvq             4 dis_int
| [p&q]>[pvq]       3 5 imp_int
| r&[[p&q]>[pvq]]   1 6 conj_int