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	$$⊢\left(\phi \wedge \psi \right)\to \chi$$
	biadanid.2	$$⊢\left(\phi \wedge \chi \right)\to \left(\psi \leftrightarrow \theta \right)$$
Assertion	biadanid	$$⊢\phi \to \left(\psi \leftrightarrow \left(\chi \wedge \theta \right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		biadanid.1	$$⊢\left(\phi \wedge \psi \right)\to \chi$$
2		biadanid.2	$$⊢\left(\phi \wedge \chi \right)\to \left(\psi \leftrightarrow \theta \right)$$
3	2	biimpa	$$⊢\left(\left(\phi \wedge \chi \right)\wedge \psi \right)\to \theta$$
4	3	an32s	$$⊢\left(\left(\phi \wedge \psi \right)\wedge \chi \right)\to \theta$$
5	1 4	mpdan	$$⊢\left(\phi \wedge \psi \right)\to \theta$$
6	1 5	jca	$$⊢\left(\phi \wedge \psi \right)\to \left(\chi \wedge \theta \right)$$
7	2	biimpar	$$⊢\left(\left(\phi \wedge \chi \right)\wedge \theta \right)\to \psi$$
8	7	anasss	$$⊢\left(\phi \wedge \left(\chi \wedge \theta \right)\right)\to \psi$$
9	6 8	impbida	$$⊢\phi \to \left(\psi \leftrightarrow \left(\chi \wedge \theta \right)\right)$$