Theorem bnj951

Description: /\ -manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	bnj951.1	$$⊢\tau \to \phi$$
	bnj951.2	$$⊢\tau \to \psi$$
	bnj951.3	$$⊢\tau \to \chi$$
	bnj951.4	$$⊢\tau \to \theta$$
Assertion	bnj951	$$⊢\tau \to \left(\phi \wedge \psi \wedge \chi \wedge \theta \right)$$

Proof

Step	Hyp	Ref	Expression
1		bnj951.1	$$⊢\tau \to \phi$$
2		bnj951.2	$$⊢\tau \to \psi$$
3		bnj951.3	$$⊢\tau \to \chi$$
4		bnj951.4	$$⊢\tau \to \theta$$
5	1 2 3	3jca	$$⊢\tau \to \left(\phi \wedge \psi \wedge \chi \right)$$
6		df-bnj17	$$⊢\left(\phi \wedge \psi \wedge \chi \wedge \theta \right)\leftrightarrow \left(\left(\phi \wedge \psi \wedge \chi \right)\wedge \theta \right)$$
7	5 4 6	sylanbrc	$$⊢\tau \to \left(\phi \wedge \psi \wedge \chi \wedge \theta \right)$$