Theorem sbcori

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

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

Proof

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