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. hlperpnel
34. perprag
35. perpdragALT
36. perpdrag
37. colperp
38. colperpexlem1
39. colperpexlem2
40. colperpexlem3
41. colperpex
42. mideulem2
43. opphllem
44. mideulem
45. midex
46. mideu