Metamath Proof Explorer
Table of Contents - 1.5.3. Axiom scheme ax-12 (Substitution)
- ax-12
- ax12v
- ax12v2
- 19.8a
- 19.8ad
- sp
- spi
- sps
- 2sp
- spsd
- 19.2g
- 19.21bi
- 19.21bbi
- 19.23bi
- nexr
- qexmid
- nf5r
- nf5rOLD
- nf5ri
- nf5rd
- spimedv
- spimefv
- nfim1
- nfan1
- 19.3t
- 19.3
- 19.9d
- 19.9t
- 19.9
- 19.21t
- 19.21
- stdpc5
- 19.21-2
- 19.23t
- 19.23
- alimd
- alrimi
- alrimdd
- alrimd
- eximd
- exlimi
- exlimd
- exlimimdd
- exlimdd
- nexd
- albid
- exbid
- nfbidf
- 19.16
- 19.17
- 19.27
- 19.28
- 19.19
- 19.36
- 19.36i
- 19.37
- 19.32
- 19.31
- 19.41
- 19.42
- 19.44
- 19.45
- spimfv
- chvarfv
- cbv3v2
- sbalex
- sb4av
- sbimd
- sbbid
- 2sbbid
- sbequ1
- sbequ2
- sbequ2OLD
- stdpc7
- sbequ12
- sbequ12r
- sbelx
- sbequ12a
- sbid
- sbcov
- sb6a
- sbid2vw
- axc16g
- axc16
- axc16gb
- axc16nf
- axc11v
- axc11rv
- drsb2
- equsalv
- equsexv
- sbft
- sbf
- sbf2
- sbh
- hbs1
- nfs1f
- sb5
- sb5OLD
- sb56OLD
- equs5av
- 2sb5
- sbco4lem
- sbco4lemOLD
- sbco4
- dfsb7
- sbn
- sbex
- nf5
- nf6
- nf5d
- nf5di
- 19.9h
- 19.21h
- 19.23h
- exlimih
- exlimdh
- equsalhw
- equsexhv
- hba1
- hbnt
- hbn
- hbnd
- hbim1
- hbimd
- hbim
- hban
- hb3an
- sbi2
- sbim
- sbrim
- sbrimv
- sblim
- sbor
- sbbi
- sblbis
- sbrbis
- sbrbif
- sbiev
- sbiedw
- sbiedwOLD
- axc7
- axc7e
- modal-b
- 19.9ht
- axc4
- axc4i
- nfal
- nfex
- hbex
- nfnf
- 19.12
- nfald
- nfexd
- nfsbv
- nfsbvOLD
- hbsbwOLD
- sbco2v
- aaan
- eeor
- cbv3v
- cbv1v
- cbv2w
- cbvaldw
- cbvexdw
- cbv3hv
- cbvalv1
- cbvexv1
- cbval2v
- cbval2vOLD
- cbvex2v
- dvelimhw
- pm11.53
- 19.12vv
- eean
- eeanv
- eeeanv
- ee4anv
- sb8v
- sb8ev
- 2sb8ev
- sb6rfv
- sbnf2
- exsb
- 2exsb
- sbbib
- sbbibvv
- sbievg
- cleljustALT
- cleljustALT2
- equs5aALT
- equs5eALT
- axc11r
- dral1v
- drex1v
- drnf1v