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

Theorem nfan 1439
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, 13-Jan-2018.)
Hypotheses
Ref Expression
nfan.1 xφ
nfan.2 xψ
Assertion
Ref Expression
nfan x(φ ψ)

Proof of Theorem nfan
StepHypRef Expression
1 nfan.1 . 2 xφ
2 nfan.2 . . 3 xψ
32a1i 9 . 2 (φ → Ⅎxψ)
41, 3nfan1 1438 1 x(φ ψ)
Colors of variables: wff set class
Syntax hints:   wa 97  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
This theorem depends on definitions:  df-bi 110  df-nf 1330
This theorem is referenced by:  nf3an  1440  cbvex2  1779  nfsbxyt  1801  sbcomxyyz  1828  nfsb4t  1872  clelab  2144  nfel  2168  2ralbida  2323  reean  2456  nfrabxy  2468  cbvrexf  2506  cbvreu  2509  cbvrab  2533  ceqsex2  2571  vtocl2gaf  2597  rspce  2628  eqvincf  2646  elrabf  2673  elrab3t  2674  rexab2  2684  morex  2702  reu2  2706  sbc2iegf  2805  rmo2ilem  2824  rmo3  2826  csbiebt  2863  csbie2t  2871  cbvrexcsf  2886  cbvreucsf  2887  cbvrabcsf  2888  nfopd  3540  eluniab  3566  dfnfc2  3572  nfdisjv  3731  nfopab  3799  cbvopab  3802  cbvopab1  3804  cbvopab2  3805  cbvopab1s  3806  mpteq12f  3811  nfmpt  3823  cbvmpt  3825  repizf2  3889  nfpo  4012  nfso  4013  peano2  4245  nfxp  4298  opeliunxp  4322  nfco  4428  elrnmpt1  4512  nfimad  4604  iota2  4820  dffun4f  4844  nffun  4850  imadif  4905  funimaexglem  4908  nffn  4921  nff  4969  nff1  5015  nffo  5030  nff1o  5049  fun11iun  5072  nffvd  5112  fv3  5122  fmptco  5255  nfiso  5371  cbvriota  5402  riota2df  5412  riota5f  5416  nfoprab  5480  mpt2eq123  5487  nfmpt2  5496  cbvoprab1  5499  cbvoprab2  5500  cbvoprab12  5501  cbvoprab3  5503  cbvmpt2x  5505  ovmpt2dxf  5549  opabex3d  5671  opabex3  5672  dfoprab4f  5742  fmpt2x  5749  nfrecs  5844  tfri3  5875  erovlem  6109  bdsepnft  7260  bdsepnfALT  7262  bj-findis  7344  strcollnft  7349
  Copyright terms: Public domain W3C validator