Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > nfim | Unicode version |
Description: If is not free in and , it is not free in . (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.) |
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 1463 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wnf 1349 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1336 ax-gen 1338 ax-4 1400 ax-ial 1427 ax-i5r 1428 |
This theorem depends on definitions: df-bi 110 df-nf 1350 |
This theorem is referenced by: nfnf 1469 nfia1 1472 sb4or 1714 cbval2 1796 nfmo1 1912 mo23 1941 euexex 1985 cbvralf 2527 vtocl2gf 2615 vtocl3gf 2616 vtoclgaf 2618 vtocl2gaf 2620 vtocl3gaf 2622 rspct 2649 rspc 2650 ralab2 2705 mob 2723 csbhypf 2885 cbvralcsf 2908 dfss2f 2936 elintab 3626 nfpo 4038 nfso 4039 nffrfor 4085 frind 4089 nfwe 4092 reusv3 4192 tfis 4306 findes 4326 dffun4f 4918 fv3 5197 tz6.12c 5203 fvmptss2 5247 fvmptssdm 5255 fvmptdf 5258 fvmptt 5262 fvmptf 5263 fmptco 5330 dff13f 5409 ovmpt2s 5624 ov2gf 5625 ovmpt2df 5632 ovi3 5637 dfoprab4f 5819 tfri3 5953 dom2lem 6252 findcard2 6346 findcard2s 6347 ac6sfi 6352 uzind4s 8533 indstr 8536 elabgft1 9917 elabgf2 9919 bj-rspgt 9925 bj-bdfindes 10074 setindis 10092 bdsetindis 10094 bj-findis 10104 bj-findes 10106 |
Copyright terms: Public domain | W3C validator |