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	⊢ ( 𝜑′ ↔ [ 𝑀 / 𝑛 ] 𝜑 )
	bnj206.2	⊢ ( 𝜓′ ↔ [ 𝑀 / 𝑛 ] 𝜓 )
	bnj206.3	⊢ ( 𝜒′ ↔ [ 𝑀 / 𝑛 ] 𝜒 )
	bnj206.4	⊢ 𝑀 ∈ V
Assertion	bnj206	⊢ ( [ 𝑀 / 𝑛 ] ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) ↔ ( 𝜑′ ∧ 𝜓′ ∧ 𝜒′ ) )

Proof

Step	Hyp	Ref	Expression
1		bnj206.1	⊢ ( 𝜑′ ↔ [ 𝑀 / 𝑛 ] 𝜑 )
2		bnj206.2	⊢ ( 𝜓′ ↔ [ 𝑀 / 𝑛 ] 𝜓 )
3		bnj206.3	⊢ ( 𝜒′ ↔ [ 𝑀 / 𝑛 ] 𝜒 )
4		bnj206.4	⊢ 𝑀 ∈ V
5		sbc3an	⊢ ( [ 𝑀 / 𝑛 ] ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) ↔ ( [ 𝑀 / 𝑛 ] 𝜑 ∧ [ 𝑀 / 𝑛 ] 𝜓 ∧ [ 𝑀 / 𝑛 ] 𝜒 ) )
6	1	bicomi	⊢ ( [ 𝑀 / 𝑛 ] 𝜑 ↔ 𝜑′ )
7	2	bicomi	⊢ ( [ 𝑀 / 𝑛 ] 𝜓 ↔ 𝜓′ )
8	3	bicomi	⊢ ( [ 𝑀 / 𝑛 ] 𝜒 ↔ 𝜒′ )
9	6 7 8	3anbi123i	⊢ ( ( [ 𝑀 / 𝑛 ] 𝜑 ∧ [ 𝑀 / 𝑛 ] 𝜓 ∧ [ 𝑀 / 𝑛 ] 𝜒 ) ↔ ( 𝜑′ ∧ 𝜓′ ∧ 𝜒′ ) )
10	5 9	bitri	⊢ ( [ 𝑀 / 𝑛 ] ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) ↔ ( 𝜑′ ∧ 𝜓′ ∧ 𝜒′ ) )