ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  nfim Structured version   GIF version

Theorem nfim 1446
Description: If x 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.)
Hypotheses
Ref Expression
nfim.1 xφ
nfim.2 xψ
Assertion
Ref Expression
nfim x(φψ)

Proof of Theorem nfim
StepHypRef Expression
1 nfim.1 . 2 xφ
2 nfim.2 . . 3 xψ
32a1i 9 . 2 (φ → Ⅎxψ)
41, 3nfim1 1445 1 x(φψ)
Colors of variables: wff set class
Syntax hints:  wi 4  wnf 1329
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1316  ax-gen 1318  ax-4 1381  ax-ial 1409  ax-i5r 1410
This theorem depends on definitions:  df-bi 110  df-nf 1330
This theorem is referenced by:  nfnf  1451  nfia1  1454  sb4or  1696  cbval2  1778  nfmo1  1894  mo23  1923  euexex  1967  cbvralf  2505  vtocl2gf  2592  vtocl3gf  2593  vtoclgaf  2595  vtocl2gaf  2597  vtocl3gaf  2599  rspct  2626  rspc  2627  ralab2  2682  mob  2700  csbhypf  2862  cbvralcsf  2885  dfss2f  2913  elintab  3600  nfpo  4012  nfso  4013  reusv3  4142  tfis  4233  findes  4253  dffun4f  4844  fv3  5122  tz6.12c  5128  fvmptss2  5172  fvmptssdm  5180  fvmptdf  5183  fvmptt  5187  fvmptf  5188  fmptco  5255  dff13f  5334  ovmpt2s  5547  ov2gf  5548  ovmpt2df  5555  ovi3  5560  dfoprab4f  5742  tfri3  5875  elabgft1  7024  elabgf2  7026  bj-rspgt  7032  bj-bdfindes  7171  setindis  7185  bdsetindis  7187  bj-findis  7197  bj-findes  7199
  Copyright terms: Public domain W3C validator