Theorem sbcani

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

	Ref	Expression
Hypotheses	sbcani.1	|- ( [. A / x ]. ph <-> ch )
	sbcani.2	|- ( [. A / x ]. ps <-> et )
Assertion	sbcani	|- ( [. A / x ]. ( ph /\ ps ) <-> ( ch /\ et ) )

Proof

Step	Hyp	Ref	Expression
1		sbcani.1	|- ( [. A / x ]. ph <-> ch )
2		sbcani.2	|- ( [. A / x ]. ps <-> et )
3		sbcan	|- ( [. A / x ]. ( ph /\ ps ) <-> ( [. A / x ]. ph /\ [. A / x ]. ps ) )
4	1 2	anbi12i	|- ( ( [. A / x ]. ph /\ [. A / x ]. ps ) <-> ( ch /\ et ) )
5	3 4	bitri	|- ( [. A / x ]. ( ph /\ ps ) <-> ( ch /\ et ) )