Description: Deduction version of clelsb3f . (Contributed by Wolf Lammen, 29-May-2023)
Ref | Expression | ||
---|---|---|---|
Hypotheses | clelsb3df.1 | ||
clelsb3df.2 | |||
Assertion | wl-clelsb3df |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | clelsb3df.1 | ||
2 | clelsb3df.2 | ||
3 | nfv | ||
4 | 2 | nfcrd | |
5 | 3 1 4 | sbco2d | |
6 | clelsb3 | ||
7 | 6 | sbbii | |
8 | clelsb3 | ||
9 | 5 7 8 | 3bitr3g |