![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nfand | Structured version Visualization version Unicode version |
Description: If in a context ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
nfand.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
nfand.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
nfand |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-an 373 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | nfand.1 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | nfand.2 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 3 | nfnd 1984 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 2, 4 | nfimd 2000 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 5 | nfnd 1984 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 1, 6 | nfxfrd 1697 |
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 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-10 1915 ax-12 1933 |
This theorem depends on definitions: df-bi 189 df-an 373 df-ex 1664 df-nf 1668 |
This theorem is referenced by: nf3and 2009 nfbid 2016 nfeld 2600 nfreud 2963 nfrmod 2964 nfrmo 2966 nfrab 2972 nfifd 3909 nfdisj 4385 dfid3 4750 nfriotad 6260 axrepndlem1 9017 axrepndlem2 9018 axunndlem1 9020 axunnd 9021 axregndlem2 9028 axinfndlem1 9030 axinfnd 9031 axacndlem4 9035 axacndlem5 9036 axacnd 9037 riotasv2d 32529 |
Copyright terms: Public domain | W3C validator |