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

Metamath Proof Explorer

Theorem bibiad

Description: Eliminate an hypothesis th in a biconditional. (Contributed by Thierry Arnoux, 4-May-2025)

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

Proof

Step Hyp Ref Expression
1 bibiad.1 ⊢ φ ∧ ψ → θ
2 bibiad.2 ⊢ φ ∧ χ → θ
3 bibiad.3 ⊢ φ ∧ θ → ψ ↔ χ
4 simpl ⊢ φ ∧ ψ → φ
5 simpr ⊢ φ ∧ ψ → ψ
6 3 biimpa ⊢ φ ∧ θ ∧ ψ → χ
7 4 1 5 6 syl21anc ⊢ φ ∧ ψ → χ
8 simpl ⊢ φ ∧ χ → φ
9 simpr ⊢ φ ∧ χ → χ
10 3 biimpar ⊢ φ ∧ θ ∧ χ → ψ
11 8 2 9 10 syl21anc ⊢ φ ∧ χ → ψ
12 7 11 impbida ⊢ φ → ψ ↔ χ