bianir

[roger witte]

I was just browsing and noticed that the published proof of bianir has has two redundant commutations of logical equivalence.  The shorter proof goes

1. bi2 .. ⊢ ((ψ ↔ φ) → (φ → ψ))

2. impcom .1.  ⊢ ((φ ∧ (ψ ↔ φ)) → ψ)

Regards

Roger

[Norman Megill]

Thanks.  I updated set.mm with your shorter proof, which you can see at http://us2.metamath.org/mpeuni/mmrecent.html#thlist
BTW "bi2" was renamed "biimpr" (for better naming consistency) on Aug. 7.

Norm