Theorem bibiad

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

	Ref	Expression
Hypotheses	bibiad.1	|- ( ( ph /\ ps ) -> th )
	bibiad.2	|- ( ( ph /\ ch ) -> th )
	bibiad.3	|- ( ( ph /\ th ) -> ( ps <-> ch ) )
Assertion	bibiad	|- ( ph -> ( ps <-> ch ) )

Proof

Step	Hyp	Ref	Expression
1		bibiad.1	|- ( ( ph /\ ps ) -> th )
2		bibiad.2	|- ( ( ph /\ ch ) -> th )
3		bibiad.3	|- ( ( ph /\ th ) -> ( ps <-> ch ) )
4		simpl	|- ( ( ph /\ ps ) -> ph )
5		simpr	|- ( ( ph /\ ps ) -> ps )
6	3	biimpa	|- ( ( ( ph /\ th ) /\ ps ) -> ch )
7	4 1 5 6	syl21anc	|- ( ( ph /\ ps ) -> ch )
8		simpl	|- ( ( ph /\ ch ) -> ph )
9		simpr	|- ( ( ph /\ ch ) -> ch )
10	3	biimpar	|- ( ( ( ph /\ th ) /\ ch ) -> ps )
11	8 2 9 10	syl21anc	|- ( ( ph /\ ch ) -> ps )
12	7 11	impbida	|- ( ph -> ( ps <-> ch ) )