Theorem bianassc

Description: An inference to merge two lists of conjuncts. (Contributed by Peter Mazsa, 24-Sep-2022)

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

Proof

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