Theorem sylbida

Description: A syllogism deduction. (Contributed by SN, 16-Jul-2024)

	Ref	Expression
Hypotheses	sylbida.1	$$⊢\phi \to \left(\psi \leftrightarrow \chi \right)$$
	sylbida.2	$$⊢\left(\phi \wedge \chi \right)\to \theta$$
Assertion	sylbida	$$⊢\left(\phi \wedge \psi \right)\to \theta$$

Proof

Step	Hyp	Ref	Expression
1		sylbida.1	$$⊢\phi \to \left(\psi \leftrightarrow \chi \right)$$
2		sylbida.2	$$⊢\left(\phi \wedge \chi \right)\to \theta$$
3	1	biimpa	$$⊢\left(\phi \wedge \psi \right)\to \chi$$
4	3 2	syldan	$$⊢\left(\phi \wedge \psi \right)\to \theta$$