Theorem simprbda

Description: Deduction eliminating a conjunct. (Contributed by NM, 22-Oct-2007)

	Ref	Expression
Hypothesis	pm3.26bda.1	$$⊢\phi \to \left(\psi \leftrightarrow \left(\chi \wedge \theta \right)\right)$$
Assertion	simprbda	$$⊢\left(\phi \wedge \psi \right)\to \chi$$

Proof

Step	Hyp	Ref	Expression
1		pm3.26bda.1	$$⊢\phi \to \left(\psi \leftrightarrow \left(\chi \wedge \theta \right)\right)$$
2	1	biimpa	$$⊢\left(\phi \wedge \psi \right)\to \left(\chi \wedge \theta \right)$$
3	2	simpld	$$⊢\left(\phi \wedge \psi \right)\to \chi$$