##
Ternary Conditional ifn

The ternary conditional ifn is an operation that chooses between two numbers depending on whether
or not a boolean expression is true. The operation is defined here.

When φ is true, (= (ifn ph a b) a) /edit/peano_new/arithmetic/common/ifn.gh/ifn1.
When φ is false, (= (ifn ph a b) b) /edit/peano_new/arithmetic/common/ifn.gh/ifn2.

Arithmetic Overview