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	|- ( ( if- ( ph , ps , ch ) \/ ( ps /\ ch ) ) <-> if- ( ph , ps , ch ) )

Proof

Step	Hyp	Ref	Expression
1		anifp	|- ( ( ps /\ ch ) -> if- ( ph , ps , ch ) )
2	1	bj-jaoi2	|- ( ( if- ( ph , ps , ch ) \/ ( ps /\ ch ) ) -> if- ( ph , ps , ch ) )
3		orc	|- ( if- ( ph , ps , ch ) -> ( if- ( ph , ps , ch ) \/ ( ps /\ ch ) ) )
4	2 3	impbii	|- ( ( if- ( ph , ps , ch ) \/ ( ps /\ ch ) ) <-> if- ( ph , ps , ch ) )