Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > nfim | GIF 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 1564 | 1 ⊢ Ⅎ𝑥(𝜑 → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 Ⅎwnf 1453 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1440 ax-gen 1442 ax-4 1503 ax-ial 1527 ax-i5r 1528 |
This theorem depends on definitions: df-bi 116 df-nf 1454 |
This theorem is referenced by: nfnf 1570 nfia1 1573 sb4or 1826 cbval2 1914 nfsbv 1940 nfmo1 2031 mo23 2060 euexex 2104 nfabdw 2331 cbvralfw 2687 cbvralf 2689 vtocl2gf 2792 vtocl3gf 2793 vtoclgaf 2795 vtocl2gaf 2797 vtocl3gaf 2799 rspct 2827 rspc 2828 ralab2 2894 mob 2912 csbhypf 3087 cbvralcsf 3111 dfss2f 3138 elintab 3842 disjiun 3984 nfpo 4286 nfso 4287 nffrfor 4333 frind 4337 nfwe 4340 reusv3 4445 tfis 4567 findes 4587 omsinds 4606 dffun4f 5214 fv3 5519 tz6.12c 5526 fvmptss2 5571 fvmptssdm 5580 fvmptdf 5583 fvmptt 5587 fvmptf 5588 fmptco 5662 dff13f 5749 ovmpos 5976 ov2gf 5977 ovmpodf 5984 ovi3 5989 dfoprab4f 6172 tfri3 6346 dom2lem 6750 findcard2 6867 findcard2s 6868 ac6sfi 6876 nfsup 6969 ismkvnex 7131 exmidfodomrlemr 7179 exmidfodomrlemrALT 7180 axpre-suploclemres 7863 uzind4s 9549 indstr 9552 supinfneg 9554 infsupneg 9555 uzsinds 10398 fimaxre2 11190 summodclem2a 11344 fsumsplitf 11371 fproddivapf 11594 fprodsplitf 11595 fprodsplit1f 11597 divalglemeunn 11880 divalglemeuneg 11882 zsupcllemstep 11900 bezoutlemmain 11953 prmind2 12074 exmidunben 12381 cnmptcom 13092 elabgft1 13813 elabgf2 13815 bj-rspgt 13821 bj-bdfindes 13984 setindis 14002 bdsetindis 14004 bj-findis 14014 bj-findes 14016 pw1nct 14036 ismkvnnlem 14084 |
Copyright terms: Public domain | W3C validator |