Are there any ternary inference rules in propositional logic?

Question

Every transformation rule I've seen in the context of propositional logic proofs have an arity of 1-2, with citations looking like

...previous
4. x        1,2 Modus Ponens
5. y        3   Double Negation Elimination

Are there any transformation rules that show up in logic proofs which operate on more than 2 propositions?

...previous
4. x        1,2,3 Some Rule

Answer 1

Some systems define:

Constructive Dilemma

$P \lor Q$

$ P \to R$

$Q \to S$

$\therefore R \lor S$

There is also:

Destructive Dilemma

$\neg R \lor \neg S$

$ P \to R$

$Q \to S$

$\therefore \neg P \lor \neg Q$

In general and theoretically, you can define inference rules involving any number of statements. In fact, they don’t even have to reflect valid inferences (… though what purpose that would have…). In practice, you’ll never see any involving 4 or more premises though, and even ternary ones are rare.

As Mauro points out in the Comments, theoretically you can do everything with just Modus Ponens and some axioms (which themselves can be seen as inferences based on zero premises). There are even systems (e.g. the Nicod system) where you can prove every propositional truth using a single operator, a single axiom, and s single inference rule.