Theorem sbcori

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

	Ref	Expression
Hypotheses	sbcori.1	⊢ ( [ 𝐴 / 𝑥 ] 𝜑 ↔ 𝜒 )
	sbcori.2	⊢ ( [ 𝐴 / 𝑥 ] 𝜓 ↔ 𝜂 )
Assertion	sbcori	⊢ ( [ 𝐴 / 𝑥 ] ( 𝜑 ∨ 𝜓 ) ↔ ( 𝜒 ∨ 𝜂 ) )

Proof

Step	Hyp	Ref	Expression
1		sbcori.1	⊢ ( [ 𝐴 / 𝑥 ] 𝜑 ↔ 𝜒 )
2		sbcori.2	⊢ ( [ 𝐴 / 𝑥 ] 𝜓 ↔ 𝜂 )
3		sbcor	⊢ ( [ 𝐴 / 𝑥 ] ( 𝜑 ∨ 𝜓 ) ↔ ( [ 𝐴 / 𝑥 ] 𝜑 ∨ [ 𝐴 / 𝑥 ] 𝜓 ) )
4	1 2	orbi12i	⊢ ( ( [ 𝐴 / 𝑥 ] 𝜑 ∨ [ 𝐴 / 𝑥 ] 𝜓 ) ↔ ( 𝜒 ∨ 𝜂 ) )
5	3 4	bitri	⊢ ( [ 𝐴 / 𝑥 ] ( 𝜑 ∨ 𝜓 ) ↔ ( 𝜒 ∨ 𝜂 ) )