Description: Distribution of class substitution over implication, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | sbcimi.1 | ||
sbcimi.2 | |||
sbcimi.3 | |||
Assertion | sbcimi |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sbcimi.1 | ||
2 | sbcimi.2 | ||
3 | sbcimi.3 | ||
4 | sbcimg | ||
5 | 1 4 | ax-mp | |
6 | 2 3 | imbi12i | |
7 | 5 6 | bitri |