Theorem bianass

Description: An inference to merge two lists of conjuncts. (Contributed by Giovanni Mascellani, 23-May-2019)

	Ref	Expression
Hypothesis	bianass.1	$$⊢\phi \leftrightarrow \left(\psi \wedge \chi \right)$$
Assertion	bianass	$$⊢\left(\eta \wedge \phi \right)\leftrightarrow \left(\left(\eta \wedge \psi \right)\wedge \chi \right)$$

Proof

Step	Hyp	Ref	Expression
1		bianass.1	$$⊢\phi \leftrightarrow \left(\psi \wedge \chi \right)$$
2	1	anbi2i	$$⊢\left(\eta \wedge \phi \right)\leftrightarrow \left(\eta \wedge \left(\psi \wedge \chi \right)\right)$$
3		anass	$$⊢\left(\left(\eta \wedge \psi \right)\wedge \chi \right)\leftrightarrow \left(\eta \wedge \left(\psi \wedge \chi \right)\right)$$
4	2 3	bitr4i	$$⊢\left(\eta \wedge \phi \right)\leftrightarrow \left(\left(\eta \wedge \psi \right)\wedge \chi \right)$$