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