Theorem sbcani

Description: Distribution of class substitution over conjunction, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019)

	Ref	Expression
Hypotheses	sbcani.1	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \chi$$
	sbcani.2	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\psi \leftrightarrow \eta$$
Assertion	sbcani	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(\phi \wedge \psi \right)\leftrightarrow \left(\chi \wedge \eta \right)$$

Proof

Step	Hyp	Ref	Expression
1		sbcani.1	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \chi$$
2		sbcani.2	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\psi \leftrightarrow \eta$$
3		sbcan	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(\phi \wedge \psi \right)\leftrightarrow \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\psi \right)$$
4	1 2	anbi12i	$$⊢\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\psi \right)\leftrightarrow \left(\chi \wedge \eta \right)$$
5	3 4	bitri	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(\phi \wedge \psi \right)\leftrightarrow \left(\chi \wedge \eta \right)$$