Theorem bnj206

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	bnj206.1	|- ( ph' <-> [. M / n ]. ph )
	bnj206.2	|- ( ps' <-> [. M / n ]. ps )
	bnj206.3	|- ( ch' <-> [. M / n ]. ch )
	bnj206.4	|- M e. _V
Assertion	bnj206	|- ( [. M / n ]. ( ph /\ ps /\ ch ) <-> ( ph' /\ ps' /\ ch' ) )

Proof

Step	Hyp	Ref	Expression
1		bnj206.1	|- ( ph' <-> [. M / n ]. ph )
2		bnj206.2	|- ( ps' <-> [. M / n ]. ps )
3		bnj206.3	|- ( ch' <-> [. M / n ]. ch )
4		bnj206.4	|- M e. _V
5		sbc3an	|- ( [. M / n ]. ( ph /\ ps /\ ch ) <-> ( [. M / n ]. ph /\ [. M / n ]. ps /\ [. M / n ]. ch ) )
6	1	bicomi	|- ( [. M / n ]. ph <-> ph' )
7	2	bicomi	|- ( [. M / n ]. ps <-> ps' )
8	3	bicomi	|- ( [. M / n ]. ch <-> ch' )
9	6 7 8	3anbi123i	|- ( ( [. M / n ]. ph /\ [. M / n ]. ps /\ [. M / n ]. ch ) <-> ( ph' /\ ps' /\ ch' ) )
10	5 9	bitri	|- ( [. M / n ]. ( ph /\ ps /\ ch ) <-> ( ph' /\ ps' /\ ch' ) )