![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > nfim | GIF version |
Description: If x 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 | ⊢ Ⅎxφ |
nfim.2 | ⊢ Ⅎxψ |
Ref | Expression |
---|---|
nfim | ⊢ Ⅎx(φ → ψ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfim.1 | . 2 ⊢ Ⅎxφ | |
2 | nfim.2 | . . 3 ⊢ Ⅎxψ | |
3 | 2 | a1i 9 | . 2 ⊢ (φ → Ⅎxψ) |
4 | 1, 3 | nfim1 1460 | 1 ⊢ Ⅎx(φ → ψ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 Ⅎwnf 1346 |
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 1333 ax-gen 1335 ax-4 1397 ax-ial 1424 ax-i5r 1425 |
This theorem depends on definitions: df-bi 110 df-nf 1347 |
This theorem is referenced by: nfnf 1466 nfia1 1469 sb4or 1711 cbval2 1793 nfmo1 1909 mo23 1938 euexex 1982 cbvralf 2521 vtocl2gf 2609 vtocl3gf 2610 vtoclgaf 2612 vtocl2gaf 2614 vtocl3gaf 2616 rspct 2643 rspc 2644 ralab2 2699 mob 2717 csbhypf 2879 cbvralcsf 2902 dfss2f 2930 elintab 3617 nfpo 4029 nfso 4030 reusv3 4158 tfis 4249 findes 4269 dffun4f 4861 fv3 5140 tz6.12c 5146 fvmptss2 5190 fvmptssdm 5198 fvmptdf 5201 fvmptt 5205 fvmptf 5206 fmptco 5273 dff13f 5352 ovmpt2s 5566 ov2gf 5567 ovmpt2df 5574 ovi3 5579 dfoprab4f 5761 tfri3 5894 dom2lem 6188 uzind4s 8309 indstr 8312 elabgft1 9252 elabgf2 9254 bj-rspgt 9260 bj-bdfindes 9409 setindis 9427 bdsetindis 9429 bj-findis 9439 bj-findes 9441 |
Copyright terms: Public domain | W3C validator |