Theorem selconj

Description: An inference for selecting one of a list of conjuncts. (Contributed by Giovanni Mascellani, 23-May-2019)

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

Proof

Step	Hyp	Ref	Expression
1		selconj.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		an12	$$⊢\left(\psi \wedge \left(\eta \wedge \chi \right)\right)\leftrightarrow \left(\eta \wedge \left(\psi \wedge \chi \right)\right)$$
4	2 3	bitr4i	$$⊢\left(\eta \wedge \phi \right)\leftrightarrow \left(\psi \wedge \left(\eta \wedge \chi \right)\right)$$