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- (φ, ψ, χ) \lor (ψ \land χ)) \leftrightarrow if- (φ, ψ, χ)$

Step	Hyp	Ref	Expression
1		orcom	$⊢ (if- (φ, ψ, χ) \lor (ψ \land χ)) \leftrightarrow ((ψ \land χ) \lor if- (φ, ψ, χ))$
2		anifp	$⊢ (ψ \land χ) \to if- (φ, ψ, χ)$
3		pm4.72	$⊢ ((ψ \land χ) \to if- (φ, ψ, χ)) \leftrightarrow (if- (φ, ψ, χ) \leftrightarrow ((ψ \land χ) \lor if- (φ, ψ, χ)))$
4	2 3	mpbi	$⊢ if- (φ, ψ, χ) \leftrightarrow ((ψ \land χ) \lor if- (φ, ψ, χ))$
5	1 4	bitr4i	$⊢ (if- (φ, ψ, χ) \lor (ψ \land χ)) \leftrightarrow if- (φ, ψ, χ)$

Metamath Proof Explorer