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 3840 disjiun 3982 nfpo 4284 nfso 4285 nffrfor 4331 frind 4335 nfwe 4338 reusv3 4443 tfis 4565 findes 4585 omsinds 4604 dffun4f 5212 fv3 5517 tz6.12c 5524 fvmptss2 5569 fvmptssdm 5578 fvmptdf 5581 fvmptt 5585 fvmptf 5586 fmptco 5659 dff13f 5746 ovmpos 5973 ov2gf 5974 ovmpodf 5981 ovi3 5986 dfoprab4f 6169 tfri3 6343 dom2lem 6746 findcard2 6863 findcard2s 6864 ac6sfi 6872 nfsup 6965 ismkvnex 7127 exmidfodomrlemr 7166 exmidfodomrlemrALT 7167 axpre-suploclemres 7850 uzind4s 9536 indstr 9539 supinfneg 9541 infsupneg 9542 uzsinds 10385 fimaxre2 11177 summodclem2a 11331 fsumsplitf 11358 fproddivapf 11581 fprodsplitf 11582 fprodsplit1f 11584 divalglemeunn 11867 divalglemeuneg 11869 zsupcllemstep 11887 bezoutlemmain 11940 prmind2 12061 exmidunben 12368 cnmptcom 13051 elabgft1 13772 elabgf2 13774 bj-rspgt 13780 bj-bdfindes 13944 setindis 13962 bdsetindis 13964 bj-findis 13974 bj-findes 13976 pw1nct 13996 ismkvnnlem 14044 |
Copyright terms: Public domain | W3C validator |