Description: Deduction version of nfsb . (Contributed by NM, 15-Feb-2013) Usage of this theorem is discouraged because it depends on ax-13 . Use nfsbv instead. (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | nfsbd.1 | |
|
nfsbd.2 | |
||
Assertion | nfsbd | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfsbd.1 | |
|
2 | nfsbd.2 | |
|
3 | 1 2 | alrimi | |
4 | nfsb4t | |
|
5 | 3 4 | syl | |
6 | axc16nf | |
|
7 | 5 6 | pm2.61d2 | |