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 ⊢ ( 𝜑 → ( 𝜓 ↔ 𝜒 ) )