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	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜒 )
	biadanid.2	⊢ ( ( 𝜑 ∧ 𝜒 ) → ( 𝜓 ↔ 𝜃 ) )
Assertion	biadanid	⊢ ( 𝜑 → ( 𝜓 ↔ ( 𝜒 ∧ 𝜃 ) ) )

Proof

Step	Hyp	Ref	Expression
1		biadanid.1	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜒 )
2		biadanid.2	⊢ ( ( 𝜑 ∧ 𝜒 ) → ( 𝜓 ↔ 𝜃 ) )
3	2	biimpa	⊢ ( ( ( 𝜑 ∧ 𝜒 ) ∧ 𝜓 ) → 𝜃 )
4	3	an32s	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) → 𝜃 )
5	1 4	mpdan	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜃 )
6	1 5	jca	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝜒 ∧ 𝜃 ) )
7	2	biimpar	⊢ ( ( ( 𝜑 ∧ 𝜒 ) ∧ 𝜃 ) → 𝜓 )
8	7	anasss	⊢ ( ( 𝜑 ∧ ( 𝜒 ∧ 𝜃 ) ) → 𝜓 )
9	6 8	impbida	⊢ ( 𝜑 → ( 𝜓 ↔ ( 𝜒 ∧ 𝜃 ) ) )