![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nfal | Structured version Visualization version Unicode version |
Description: If ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
nfal.1 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
nfal |
![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfal.1 |
. . . 4
![]() ![]() ![]() ![]() | |
2 | 1 | nfri 1972 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | hbal 1939 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | 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-11 1937 ax-12 1950 |
This theorem depends on definitions: df-bi 190 df-ex 1672 df-nf 1676 |
This theorem is referenced by: nfnf 2051 nfald 2053 nfa2 2055 aaan 2074 cbv3v 2078 pm11.53 2090 19.12vv 2091 cbv3 2121 cbval2 2133 nfsb4t 2238 euf 2327 mo2 2328 2eu3 2404 bm1.1 2456 nfnfc1 2615 nfnfc 2621 nfnfcALT 2622 sbcnestgf 3788 dfnfc2 4208 nfdisj 4378 nfdisj1 4379 axrep1 4509 axrep2 4510 axrep3 4511 axrep4 4512 nffr 4813 zfcndrep 9057 zfcndinf 9061 mreexexd 15632 mptelee 25004 mo5f 28199 19.12b 30519 bj-cbv2v 31399 bj-cbval2v 31404 bj-axrep1 31469 bj-axrep2 31470 bj-axrep3 31471 bj-axrep4 31472 ax11-pm2 31504 bj-nfnfc 31530 wl-sb8t 31950 wl-mo2tf 31970 wl-eutf 31972 wl-mo2t 31974 wl-mo3t 31975 wl-sb8eut 31976 mpt2bi123f 32470 pm11.57 36809 pm11.59 36811 |
Copyright terms: Public domain | W3C validator |