Theorem sbcori

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

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

Proof

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