Metamath Proof Explorer
Table of Contents - 20.37. Mathbox for Andrew Salmon
- Principia Mathematica * 10
- pm10.12
- pm10.14
- pm10.251
- pm10.252
- pm10.253
- albitr
- pm10.42
- pm10.52
- pm10.53
- pm10.541
- pm10.542
- pm10.55
- pm10.56
- pm10.57
- Principia Mathematica * 11
- 2alanimi
- 2al2imi
- pm11.11
- pm11.12
- 19.21vv
- 2alim
- 2albi
- 2exim
- 2exbi
- spsbce-2
- 19.33-2
- 19.36vv
- 19.31vv
- 19.37vv
- 19.28vv
- pm11.52
- aaanv
- pm11.57
- pm11.58
- pm11.59
- pm11.6
- pm11.61
- pm11.62
- pm11.63
- pm11.7
- pm11.71
- Predicate Calculus
- sbeqal1
- sbeqal1i
- sbeqal2i
- axc5c4c711
- axc5c4c711toc5
- axc5c4c711toc4
- axc5c4c711toc7
- axc5c4c711to11
- axc11next
- Principia Mathematica * 13 and * 14
- pm13.13a
- pm13.13b
- pm13.14
- pm13.192
- pm13.193
- pm13.194
- pm13.195
- pm13.196a
- 2sbc6g
- 2sbc5g
- iotain
- iotaexeu
- iotasbc
- iotasbc2
- pm14.12
- pm14.122a
- pm14.122b
- pm14.122c
- pm14.123a
- pm14.123b
- pm14.123c
- pm14.18
- iotaequ
- iotavalb
- iotasbc5
- pm14.24
- iotavalsb
- sbiota1
- sbaniota
- eubiOLD
- iotasbcq
- Set Theory
- elnev
- rusbcALT
- compeq
- compne
- compab
- conss2
- conss1
- ralbidar
- rexbidar
- dropab1
- dropab2
- ipo0
- ifr0
- ordpss
- fvsb
- fveqsb
- xpexb
- trelpss
- Arithmetic
- addcomgi
- Geometry
- cplusr
- cminusr
- ctimesr
- cptdfc
- crr3c
- cline3
- df-addr
- df-subr
- df-mulv
- addrval
- subrval
- mulvval
- addrfv
- subrfv
- mulvfv
- addrfn
- subrfn
- mulvfn
- addrcom
- df-ptdf
- df-rr3
- df-line3