![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nfan1 | Structured version Visualization version Unicode version |
Description: A closed form of nfan 2031. (Contributed by Mario Carneiro, 3-Oct-2016.) |
Ref | Expression |
---|---|
nfan1.1 |
![]() ![]() ![]() ![]() |
nfan1.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
nfan1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfan1.2 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | nfrd 1973 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | imdistani 704 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | nfan1.1 |
. . . 4
![]() ![]() ![]() ![]() | |
5 | 4 | 19.28 2027 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 3, 5 | sylibr 217 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 6 | nfi 1682 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-12 1950 |
This theorem depends on definitions: df-bi 190 df-an 378 df-ex 1672 df-nf 1676 |
This theorem is referenced by: nfan 2031 ralcom2 2941 sbcralt 3328 sbcrext 3329 csbiebt 3369 riota5f 6294 axrepndlem1 9035 axrepndlem2 9036 axunnd 9039 axpowndlem2 9041 axpowndlem3 9042 axpowndlem4 9043 axregndlem2 9046 axinfndlem1 9048 axinfnd 9049 axacndlem4 9053 axacndlem5 9054 axacnd 9055 fproddivf 14118 wl-sbcom2d-lem1 31959 wl-mo2df 31969 wl-eudf 31971 wl-mo3t 31975 wl-ax11-lem4 31982 wl-ax11-lem6 31984 |
Copyright terms: Public domain | W3C validator |