![]() |
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 1571 | 1 ⊢ Ⅎ𝑥(𝜑 → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 Ⅎwnf 1460 |
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 3998 nfpo 4301 nfso 4302 nffrfor 4348 frind 4352 nfwe 4355 reusv3 4460 tfis 4582 findes 4602 omsinds 4621 dffun4f 5232 fv3 5538 tz6.12c 5545 fvmptss2 5591 fvmptssdm 5600 fvmptdf 5603 fvmptt 5607 fvmptf 5608 fmptco 5682 dff13f 5770 ovmpos 5997 ov2gf 5998 ovmpodf 6005 ovi3 6010 dfoprab4f 6193 tfri3 6367 dom2lem 6771 findcard2 6888 findcard2s 6889 ac6sfi 6897 nfsup 6990 ismkvnex 7152 exmidfodomrlemr 7200 exmidfodomrlemrALT 7201 axpre-suploclemres 7899 uzind4s 9589 indstr 9592 supinfneg 9594 infsupneg 9595 uzsinds 10441 fimaxre2 11234 summodclem2a 11388 fsumsplitf 11415 fproddivapf 11638 fprodsplitf 11639 fprodsplit1f 11641 divalglemeunn 11925 divalglemeuneg 11927 zsupcllemstep 11945 bezoutlemmain 11998 prmind2 12119 exmidunben 12426 cnmptcom 13768 lgseisenlem2 14421 elabgft1 14500 elabgf2 14502 bj-rspgt 14508 bj-bdfindes 14671 setindis 14689 bdsetindis 14691 bj-findis 14701 bj-findes 14703 pw1nct 14722 ismkvnnlem 14770 |
Copyright terms: Public domain | W3C validator |