![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > nfim | Unicode version |
Description: If ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
nfim.1 |
![]() ![]() ![]() ![]() |
nfim.2 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
nfim |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfim.1 |
. 2
![]() ![]() ![]() ![]() | |
2 | nfim.2 |
. . 3
![]() ![]() ![]() ![]() | |
3 | 2 | a1i 9 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | nfim1 1571 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1447 ax-gen 1449 ax-4 1510 ax-ial 1534 ax-i5r 1535 |
This theorem depends on definitions: df-bi 117 df-nf 1461 |
This theorem is referenced by: nfnf 1577 nfia1 1580 sb4or 1833 cbval2 1921 nfsbv 1947 nfmo1 2038 mo23 2067 euexex 2111 nfabdw 2338 cbvralfw 2694 cbvralf 2696 vtocl2gf 2799 vtocl3gf 2800 vtoclgaf 2802 vtocl2gaf 2804 vtocl3gaf 2806 rspct 2834 rspc 2835 ralab2 2901 mob 2919 csbhypf 3095 cbvralcsf 3119 dfss2f 3146 elintab 3855 disjiun 3997 nfpo 4300 nfso 4301 nffrfor 4347 frind 4351 nfwe 4354 reusv3 4459 tfis 4581 findes 4601 omsinds 4620 dffun4f 5231 fv3 5537 tz6.12c 5544 fvmptss2 5590 fvmptssdm 5599 fvmptdf 5602 fvmptt 5606 fvmptf 5607 fmptco 5681 dff13f 5768 ovmpos 5995 ov2gf 5996 ovmpodf 6003 ovi3 6008 dfoprab4f 6191 tfri3 6365 dom2lem 6769 findcard2 6886 findcard2s 6887 ac6sfi 6895 nfsup 6988 ismkvnex 7150 exmidfodomrlemr 7198 exmidfodomrlemrALT 7199 axpre-suploclemres 7897 uzind4s 9586 indstr 9589 supinfneg 9591 infsupneg 9592 uzsinds 10437 fimaxre2 11228 summodclem2a 11382 fsumsplitf 11409 fproddivapf 11632 fprodsplitf 11633 fprodsplit1f 11635 divalglemeunn 11918 divalglemeuneg 11920 zsupcllemstep 11938 bezoutlemmain 11991 prmind2 12112 exmidunben 12419 cnmptcom 13669 elabgft1 14390 elabgf2 14392 bj-rspgt 14398 bj-bdfindes 14561 setindis 14579 bdsetindis 14581 bj-findis 14591 bj-findes 14593 pw1nct 14612 ismkvnnlem 14660 |
Copyright terms: Public domain | W3C validator |