Theorem bj-consensusALT

Description: Alternate proof of bj-consensus . (Contributed by BJ, 30-Sep-2019) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	bj-consensusALT	|- ( ( if- ( ph , ps , ch ) \/ ( ps /\ ch ) ) <-> if- ( ph , ps , ch ) )

Proof

Step	Hyp	Ref	Expression
1		orcom	|- ( ( if- ( ph , ps , ch ) \/ ( ps /\ ch ) ) <-> ( ( ps /\ ch ) \/ if- ( ph , ps , ch ) ) )
2		anifp	|- ( ( ps /\ ch ) -> if- ( ph , ps , ch ) )
3		pm4.72	|- ( ( ( ps /\ ch ) -> if- ( ph , ps , ch ) ) <-> ( if- ( ph , ps , ch ) <-> ( ( ps /\ ch ) \/ if- ( ph , ps , ch ) ) ) )
4	2 3	mpbi	|- ( if- ( ph , ps , ch ) <-> ( ( ps /\ ch ) \/ if- ( ph , ps , ch ) ) )
5	1 4	bitr4i	|- ( ( if- ( ph , ps , ch ) \/ ( ps /\ ch ) ) <-> if- ( ph , ps , ch ) )