Metamath Proof Explorer

Theorem biadaniALT

Description: Alternate proof of biadani not using biadan . (Contributed by BJ, 4-Mar-2023) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis biadani.1 ⊢ φ → ψ
Assertion biadaniALT ⊢ ψ → φ ↔ χ ↔ φ ↔ ψ ∧ χ

Proof

Step Hyp Ref Expression
1 biadani.1 ⊢ φ → ψ
2 pm5.32 ⊢ ψ → φ ↔ χ ↔ ψ ∧ φ ↔ ψ ∧ χ
3 1 pm4.71ri ⊢ φ ↔ ψ ∧ φ
4 3 bibi1i ⊢ φ ↔ ψ ∧ χ ↔ ψ ∧ φ ↔ ψ ∧ χ
5 2 4 bitr4i ⊢ ψ → φ ↔ χ ↔ φ ↔ ψ ∧ χ