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- ( 𝜑 , 𝜓 , 𝜒 ) ∨ ( 𝜓 ∧ 𝜒 ) ) ↔ if- ( 𝜑 , 𝜓 , 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		anifp	⊢ ( ( 𝜓 ∧ 𝜒 ) → if- ( 𝜑 , 𝜓 , 𝜒 ) )
2	1	bj-jaoi2	⊢ ( ( if- ( 𝜑 , 𝜓 , 𝜒 ) ∨ ( 𝜓 ∧ 𝜒 ) ) → if- ( 𝜑 , 𝜓 , 𝜒 ) )
3		orc	⊢ ( if- ( 𝜑 , 𝜓 , 𝜒 ) → ( if- ( 𝜑 , 𝜓 , 𝜒 ) ∨ ( 𝜓 ∧ 𝜒 ) ) )
4	2 3	impbii	⊢ ( ( if- ( 𝜑 , 𝜓 , 𝜒 ) ∨ ( 𝜓 ∧ 𝜒 ) ) ↔ if- ( 𝜑 , 𝜓 , 𝜒 ) )