This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem biadanii

Description: Inference associated with biadani . Add a conjunction to an equivalence. (Contributed by Jeff Madsen, 20-Jun-2011) (Proof shortened by BJ, 4-Mar-2023)

Ref Expression
Hypotheses biadani.1 ⊢ φ → ψ
biadanii.2 ⊢ ψ → φ ↔ χ
Assertion biadanii ⊢ φ ↔ ψ ∧ χ

Proof

Step Hyp Ref Expression
1 biadani.1 ⊢ φ → ψ
2 biadanii.2 ⊢ ψ → φ ↔ χ
3 1 biadani ⊢ ψ → φ ↔ χ ↔ φ ↔ ψ ∧ χ
4 2 3 mpbi ⊢ φ ↔ ψ ∧ χ