Description: Deduction form of nfif . (Contributed by NM, 15-Feb-2013) (Revised by Mario Carneiro, 13-Oct-2016)
Ref | Expression | ||
---|---|---|---|
Hypotheses | nfifd.2 | |
|
nfifd.3 | |
||
nfifd.4 | |
||
Assertion | nfifd | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfifd.2 | |
|
2 | nfifd.3 | |
|
3 | nfifd.4 | |
|
4 | dfif2 | |
|
5 | nfv | |
|
6 | 3 | nfcrd | |
7 | 6 1 | nfimd | |
8 | 2 | nfcrd | |
9 | 8 1 | nfand | |
10 | 7 9 | nfimd | |
11 | 5 10 | nfabdw | |
12 | 4 11 | nfcxfrd | |