Metamath Proof Explorer

Theorem had1OLD

Description: Obsolete version of had1 as of 10-Aug-2026. (Contributed by Mario Carneiro, 4-Sep-2016) (Proof shortened by Wolf Lammen, 11-Jul-2020) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion had1OLD ⊢ φ → hadd φ ψ χ ↔ ψ ↔ χ

Proof

Step Hyp Ref Expression
1 hadrot ⊢ hadd φ ψ χ ↔ hadd ψ χ φ
2 hadbi ⊢ hadd ψ χ φ ↔ ψ ↔ χ ↔ φ
3 1 2 bitri ⊢ hadd φ ψ χ ↔ ψ ↔ χ ↔ φ
4 biass ⊢ hadd φ ψ χ ↔ ψ ↔ χ ↔ φ ↔ hadd φ ψ χ ↔ ψ ↔ χ ↔ φ
5 3 4 mpbir ⊢ hadd φ ψ χ ↔ ψ ↔ χ ↔ φ
6 5 biimpri ⊢ φ → hadd φ ψ χ ↔ ψ ↔ χ