Metamath Proof Explorer

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- φ ψ χ ∨ ψ ∧ χ ↔ if- φ ψ χ

Proof

Step Hyp Ref Expression
1 orcom ⊢ if- φ ψ χ ∨ ψ ∧ χ ↔ ψ ∧ χ ∨ if- φ ψ χ
2 anifp ⊢ ψ ∧ χ → if- φ ψ χ
3 pm4.72 ⊢ ψ ∧ χ → if- φ ψ χ ↔ if- φ ψ χ ↔ ψ ∧ χ ∨ if- φ ψ χ
4 2 3 mpbi ⊢ if- φ ψ χ ↔ ψ ∧ χ ∨ if- φ ψ χ
5 1 4 bitr4i ⊢ if- φ ψ χ ∨ ψ ∧ χ ↔ if- φ ψ χ