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

Theorem nfim 1480
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 1479 1 𝑥(𝜑𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wnf 1365
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-4 1416  ax-ial 1443  ax-i5r 1444
This theorem depends on definitions:  df-bi 114  df-nf 1366
This theorem is referenced by:  nfnf  1485  nfia1  1488  sb4or  1730  cbval2  1812  nfmo1  1928  mo23  1957  euexex  2001  cbvralf  2544  vtocl2gf  2632  vtocl3gf  2633  vtoclgaf  2635  vtocl2gaf  2637  vtocl3gaf  2639  rspct  2666  rspc  2667  ralab2  2728  mob  2746  csbhypf  2913  cbvralcsf  2936  dfss2f  2964  elintab  3654  nfpo  4066  nfso  4067  nffrfor  4113  frind  4117  nfwe  4120  reusv3  4220  tfis  4334  findes  4354  dffun4f  4946  fv3  5225  tz6.12c  5231  fvmptss2  5275  fvmptssdm  5283  fvmptdf  5286  fvmptt  5290  fvmptf  5291  fmptco  5358  dff13f  5437  ovmpt2s  5652  ov2gf  5653  ovmpt2df  5660  ovi3  5665  dfoprab4f  5847  tfri3  5984  dom2lem  6283  findcard2  6377  findcard2s  6378  ac6sfi  6383  nfsup  6398  uzind4s  8629  indstr  8632  divalglemeunn  10233  divalglemeuneg  10235  elabgft1  10304  elabgf2  10306  bj-rspgt  10312  bj-bdfindes  10461  setindis  10479  bdsetindis  10481  bj-findis  10491  bj-findes  10493
  Copyright terms: Public domain W3C validator