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 1558 | 1 ⊢ Ⅎ𝑥(𝜑 → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 Ⅎwnf 1447 |
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 1434 ax-gen 1436 ax-4 1497 ax-ial 1521 ax-i5r 1522 |
This theorem depends on definitions: df-bi 116 df-nf 1448 |
This theorem is referenced by: nfnf 1564 nfia1 1567 sb4or 1820 cbval2 1908 nfsbv 1934 nfmo1 2025 mo23 2054 euexex 2098 nfabdw 2325 cbvralfw 2681 cbvralf 2682 vtocl2gf 2783 vtocl3gf 2784 vtoclgaf 2786 vtocl2gaf 2788 vtocl3gaf 2790 rspct 2818 rspc 2819 ralab2 2885 mob 2903 csbhypf 3078 cbvralcsf 3102 dfss2f 3128 elintab 3829 disjiun 3971 nfpo 4273 nfso 4274 nffrfor 4320 frind 4324 nfwe 4327 reusv3 4432 tfis 4554 findes 4574 omsinds 4593 dffun4f 5198 fv3 5503 tz6.12c 5510 fvmptss2 5555 fvmptssdm 5564 fvmptdf 5567 fvmptt 5571 fvmptf 5572 fmptco 5645 dff13f 5732 ovmpos 5956 ov2gf 5957 ovmpodf 5964 ovi3 5969 dfoprab4f 6153 tfri3 6326 dom2lem 6729 findcard2 6846 findcard2s 6847 ac6sfi 6855 nfsup 6948 ismkvnex 7110 exmidfodomrlemr 7149 exmidfodomrlemrALT 7150 axpre-suploclemres 7833 uzind4s 9519 indstr 9522 supinfneg 9524 infsupneg 9525 uzsinds 10367 fimaxre2 11154 summodclem2a 11308 fsumsplitf 11335 fproddivapf 11558 fprodsplitf 11559 fprodsplit1f 11561 divalglemeunn 11843 divalglemeuneg 11845 zsupcllemstep 11863 bezoutlemmain 11916 prmind2 12031 exmidunben 12302 cnmptcom 12845 elabgft1 13500 elabgf2 13502 bj-rspgt 13508 bj-bdfindes 13672 setindis 13690 bdsetindis 13692 bj-findis 13702 bj-findes 13704 pw1nct 13724 ismkvnnlem 13772 |
Copyright terms: Public domain | W3C validator |