Metamath Proof Explorer

Table of Contents - 16.2.12. Right angles

1. crag
2. df-rag
3. cperpg
4. df-perpg
5. israg
6. ragcom
7. ragcol
8. ragmir
9. mirrag
10. ragtrivb
11. ragflat2
12. ragflat
13. ragtriva
14. ragflat3
15. ragcgr
16. motrag
17. ragncol
18. perpln1
19. perpln2
20. isperp
21. perpcom
22. perpneq
23. isperp2
24. isperp2d
25. ragperp
26. footexALT
27. footexlem1
28. footexlem2
29. footex
30. foot
31. footne
32. footeq
33. perpin
34. hlperpnel
35. perprag
36. perpdragALT
37. perpdrag
38. colperp
39. colperpexlem1
40. colperpexlem2
41. colperpexlem3
42. colperpex
43. mideulem2
44. opphllem
45. mideulem
46. midex
47. mideu