Description: A friendship graph is connected, see remark 1 in MertziosUnger p. 153 (after Proposition 1): "An arbitrary friendship graph has to be connected, ... ". (Contributed by Alexander van der Vekens, 6-Dec-2017) (Revised by AV, 1-Apr-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | frgrconngr | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid | |
|
2 | 1 | 2pthfrgr | |
3 | spthonpthon | |
|
4 | 3 | adantr | |
5 | 4 | 2eximi | |
6 | 5 | 2ralimi | |
7 | 2 6 | syl | |
8 | 1 | isconngr1 | |
9 | 7 8 | mpbird | |