Description: The property of being a finite simple graph. (Contributed by AV, 3-Jan-2020) (Revised by AV, 21-Oct-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | isfusgr.v | ||
isfusgrf1.i | |||
Assertion | isfusgrf1 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | isfusgr.v | ||
2 | isfusgrf1.i | ||
3 | 1 | isfusgr | |
4 | 1 2 | isusgrs | |
5 | 4 | anbi1d | |
6 | 3 5 | syl5bb |