Metamath Proof Explorer


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 ) )