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

Theorem nfim 1507
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.)
Hypotheses
Ref Expression
nfim.1 𝑥𝜑
nfim.2 𝑥𝜓
Assertion
Ref Expression
nfim 𝑥(𝜑𝜓)

Proof of Theorem nfim
StepHypRef Expression
1 nfim.1 . 2 𝑥𝜑
2 nfim.2 . . 3 𝑥𝜓
32a1i 9 . 2 (𝜑 → Ⅎ𝑥𝜓)
41, 3nfim1 1506 1 𝑥(𝜑𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wnf 1392
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1379  ax-gen 1381  ax-4 1443  ax-ial 1470  ax-i5r 1471
This theorem depends on definitions:  df-bi 115  df-nf 1393
This theorem is referenced by:  nfnf  1512  nfia1  1515  sb4or  1758  cbval2  1841  nfmo1  1957  mo23  1986  euexex  2030  cbvralf  2580  vtocl2gf  2674  vtocl3gf  2675  vtoclgaf  2677  vtocl2gaf  2679  vtocl3gaf  2681  rspct  2708  rspc  2709  ralab2  2770  mob  2788  csbhypf  2955  cbvralcsf  2979  dfss2f  3005  elintab  3682  nfpo  4102  nfso  4103  nffrfor  4149  frind  4153  nfwe  4156  reusv3  4256  tfis  4371  findes  4391  omsinds  4408  dffun4f  4997  fv3  5291  tz6.12c  5297  fvmptss2  5342  fvmptssdm  5350  fvmptdf  5353  fvmptt  5357  fvmptf  5358  fmptco  5427  dff13f  5510  ovmpt2s  5725  ov2gf  5726  ovmpt2df  5733  ovi3  5738  dfoprab4f  5920  tfri3  6086  dom2lem  6441  findcard2  6557  findcard2s  6558  ac6sfi  6566  nfsup  6631  exmidfodomrlemr  6772  exmidfodomrlemrALT  6773  uzind4s  9010  indstr  9013  supinfneg  9015  infsupneg  9016  uzsinds  9776  fimaxre2  10551  isummolem2a  10660  divalglemeunn  10796  divalglemeuneg  10798  zsupcllemstep  10816  bezoutlemmain  10862  prmind2  10977  elabgft1  11116  elabgf2  11118  bj-rspgt  11124  bj-bdfindes  11282  setindis  11300  bdsetindis  11302  bj-findis  11312  bj-findes  11314
  Copyright terms: Public domain W3C validator