Theorem bj-consensus

Description: Version of consensus expressed using the conditional operator. (Remark: it may be better to express it as consensus , using only binary connectives, and hinting at the fact that it is a Boolean algebra identity, like the absorption identities.) (Contributed by BJ, 30-Sep-2019)

	Ref	Expression
Assertion	bj-consensus	$$⊢\left(if-\left(\phi ,\psi ,\chi \right)\vee \left(\psi \wedge \chi \right)\right)\leftrightarrow if-\left(\phi ,\psi ,\chi \right)$$

Proof

Step	Hyp	Ref	Expression
1		anifp	$$⊢\left(\psi \wedge \chi \right)\to if-\left(\phi ,\psi ,\chi \right)$$
2	1	bj-jaoi2	$$⊢\left(if-\left(\phi ,\psi ,\chi \right)\vee \left(\psi \wedge \chi \right)\right)\to if-\left(\phi ,\psi ,\chi \right)$$
3		orc	$$⊢if-\left(\phi ,\psi ,\chi \right)\to \left(if-\left(\phi ,\psi ,\chi \right)\vee \left(\psi \wedge \chi \right)\right)$$
4	2 3	impbii	$$⊢\left(if-\left(\phi ,\psi ,\chi \right)\vee \left(\psi \wedge \chi \right)\right)\leftrightarrow if-\left(\phi ,\psi ,\chi \right)$$