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

Metamath Proof Explorer

Theorem biadanid

Description: Deduction associated with biadani . Add a conjunction to an equivalence. (Contributed by Thierry Arnoux, 16-Jun-2024)

Ref Expression
Hypotheses biadanid.1 ⊢ φ ∧ ψ → χ
biadanid.2 ⊢ φ ∧ χ → ψ ↔ θ
Assertion biadanid ⊢ φ → ψ ↔ χ ∧ θ

Proof

Step Hyp Ref Expression
1 biadanid.1 ⊢ φ ∧ ψ → χ
2 biadanid.2 ⊢ φ ∧ χ → ψ ↔ θ
3 2 biimpa ⊢ φ ∧ χ ∧ ψ → θ
4 3 an32s ⊢ φ ∧ ψ ∧ χ → θ
5 1 4 mpdan ⊢ φ ∧ ψ → θ
6 1 5 jca ⊢ φ ∧ ψ → χ ∧ θ
7 2 biimpar ⊢ φ ∧ χ ∧ θ → ψ
8 7 anasss ⊢ φ ∧ χ ∧ θ → ψ
9 6 8 impbida ⊢ φ → ψ ↔ χ ∧ θ