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 1550 | 1 ⊢ Ⅎ𝑥(𝜑 → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 Ⅎwnf 1436 |
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 1423 ax-gen 1425 ax-4 1487 ax-ial 1514 ax-i5r 1515 |
This theorem depends on definitions: df-bi 116 df-nf 1437 |
This theorem is referenced by: nfnf 1556 nfia1 1559 sb4or 1805 cbval2 1891 nfmo1 2009 mo23 2038 euexex 2082 cbvralf 2646 vtocl2gf 2743 vtocl3gf 2744 vtoclgaf 2746 vtocl2gaf 2748 vtocl3gaf 2750 rspct 2777 rspc 2778 ralab2 2843 mob 2861 csbhypf 3033 cbvralcsf 3057 dfss2f 3083 elintab 3777 disjiun 3919 nfpo 4218 nfso 4219 nffrfor 4265 frind 4269 nfwe 4272 reusv3 4376 tfis 4492 findes 4512 omsinds 4530 dffun4f 5134 fv3 5437 tz6.12c 5444 fvmptss2 5489 fvmptssdm 5498 fvmptdf 5501 fvmptt 5505 fvmptf 5506 fmptco 5579 dff13f 5664 ovmpos 5887 ov2gf 5888 ovmpodf 5895 ovi3 5900 dfoprab4f 6084 tfri3 6257 dom2lem 6659 findcard2 6776 findcard2s 6777 ac6sfi 6785 nfsup 6872 ismkvnex 7022 exmidfodomrlemr 7051 exmidfodomrlemrALT 7052 axpre-suploclemres 7702 uzind4s 9378 indstr 9381 supinfneg 9383 infsupneg 9384 uzsinds 10208 fimaxre2 10991 summodclem2a 11143 fsumsplitf 11170 divalglemeunn 11607 divalglemeuneg 11609 zsupcllemstep 11627 bezoutlemmain 11675 prmind2 11790 exmidunben 11928 cnmptcom 12456 elabgft1 12974 elabgf2 12976 bj-rspgt 12982 bj-bdfindes 13136 setindis 13154 bdsetindis 13156 bj-findis 13166 bj-findes 13168 |
Copyright terms: Public domain | W3C validator |