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