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

Theorem nfim 1438
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 1437 1 x(φψ)
Colors of variables: wff set class
Syntax hints:  wi 4  wnf 1323
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 1310  ax-gen 1312  ax-4 1374  ax-ial 1401  ax-i5r 1402
This theorem depends on definitions:  df-bi 110  df-nf 1324
This theorem is referenced by:  nfnf  1443  nfia1  1446  sb4or  1688  cbval2  1770  nfmo1  1886  mo23  1915  euexex  1959  cbvralf  2497  vtocl2gf  2584  vtocl3gf  2585  vtoclgaf  2587  vtocl2gaf  2589  vtocl3gaf  2591  rspct  2618  rspc  2619  ralab2  2674  mob  2692  csbhypf  2854  cbvralcsf  2877  dfss2f  2905  elintab  3590  nfpo  4002  nfso  4003  reusv3  4131  tfis  4222  findes  4242  dffun4f  4833  fv3  5111  tz6.12c  5117  fvmptss2  5161  fvmptssdm  5169  fvmptdf  5172  fvmptt  5176  fvmptf  5177  fmptco  5244  dff13f  5323  ovmpt2s  5536  ov2gf  5537  ovmpt2df  5544  ovi3  5549  dfoprab4f  5731  tfri3  5864  elabgft1  8254  elabgf2  8256  bj-rspgt  8262  bj-bdfindes  8405  setindis  8419  bdsetindis  8421  bj-findis  8431  bj-findes  8433
  Copyright terms: Public domain W3C validator