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	|- ( ( ph /\ ps ) -> ch )
	biadanid.2	|- ( ( ph /\ ch ) -> ( ps <-> th ) )
Assertion	biadanid	|- ( ph -> ( ps <-> ( ch /\ th ) ) )

Proof

Step	Hyp	Ref	Expression
1		biadanid.1	|- ( ( ph /\ ps ) -> ch )
2		biadanid.2	|- ( ( ph /\ ch ) -> ( ps <-> th ) )
3	2	biimpa	|- ( ( ( ph /\ ch ) /\ ps ) -> th )
4	3	an32s	|- ( ( ( ph /\ ps ) /\ ch ) -> th )
5	1 4	mpdan	|- ( ( ph /\ ps ) -> th )
6	1 5	jca	|- ( ( ph /\ ps ) -> ( ch /\ th ) )
7	2	biimpar	|- ( ( ( ph /\ ch ) /\ th ) -> ps )
8	7	anasss	|- ( ( ph /\ ( ch /\ th ) ) -> ps )
9	6 8	impbida	|- ( ph -> ( ps <-> ( ch /\ th ) ) )